# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257332842 -3600
# Node ID b2fd070c88338cbd664ff6919cc90556a9831adf
# Parent  bdedfb51778d02fdc46d6732524827e28846e70f
slightly tuned

diff -r bdedfb51778d -r b2fd070c8833 quotient_def.ML
--- a/quotient_def.ML	Wed Nov 04 11:59:48 2009 +0100
+++ b/quotient_def.ML	Wed Nov 04 12:07:22 2009 +0100
@@ -15,6 +15,7 @@
 structure Quotient_Def: QUOTIENT_DEF =
 struct
 
+(* wrapper for define *)
 fun define name mx attr rhs lthy =
 let
   val ((rhs, (_ , thm)), lthy') =
@@ -120,6 +121,8 @@
   | diffs _ _ = error "Unequal length of type arguments"
 
 
+(* sanity check that the calculated quotient environment
+   matches with the stored quotient environment. *)
 fun error_msg lthy (qty, rty) =
 let 
   val qtystr = quote (Syntax.string_of_typ lthy qty)
@@ -130,21 +133,21 @@
 
 fun sanity_chk lthy qenv =
 let
-   val qenv' = Quotient_Info.mk_qenv lthy
-   val thy = ProofContext.theory_of lthy
+  val qenv' = Quotient_Info.mk_qenv lthy
+  val thy = ProofContext.theory_of lthy
 
-   fun is_inst thy (qty, rty) (qty', rty') =
-   if Sign.typ_instance thy (qty, qty')
-   then let
-          val inst = Sign.typ_match thy (qty', qty) Vartab.empty
-        in
-          rty = Envir.subst_type inst rty'
-        end
-   else false
+  fun is_inst thy (qty, rty) (qty', rty') =
+  if Sign.typ_instance thy (qty, qty')
+  then let
+         val inst = Sign.typ_match thy (qty', qty) Vartab.empty
+       in
+         rty = Envir.subst_type inst rty'       
+       end
+  else false
 
-   fun chk_inst (qty, rty) = 
-     if exists (is_inst thy (qty, rty)) qenv' then true
-     else error_msg lthy (qty, rty)
+  fun chk_inst (qty, rty) = 
+    if exists (is_inst thy (qty, rty)) qenv' then true
+    else error_msg lthy (qty, rty)
 in
   forall chk_inst qenv
 end
@@ -162,13 +165,6 @@
   make_def bind rhs qty mx attr qenv lthy 
 end
 
-
-val quotdef_parser =
-  (OuterParse.binding --
-    (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ -- 
-      OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) -- 
-       (SpecParse.opt_thm_name ":" -- OuterParse.prop)
-
 fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy = 
 let
   val qty  = (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystr
@@ -177,6 +173,13 @@
   quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd
 end
 
+
+val quotdef_parser =
+  (OuterParse.binding --
+    (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ -- 
+      OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) -- 
+       (SpecParse.opt_thm_name ":" -- OuterParse.prop)
+
 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
   OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)