src/HOL/Tools/Quotient/quotient_def.ML

--- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Jan 07 14:58:15 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Jan 07 15:35:00 2011 +0100
@@ -34,75 +34,75 @@
 
    It stores the qconst_info in the qconsts data slot.
 
-   Restriction: At the moment the left- and right-hand 
-   side of the definition must be a constant. 
+   Restriction: At the moment the left- and right-hand
+   side of the definition must be a constant.
 *)
-fun error_msg bind str = 
-let 
-  val name = Binding.name_of bind
-  val pos = Position.str_of (Binding.pos_of bind)
-in
-  error ("Head of quotient_definition " ^ 
-    quote str ^ " differs from declaration " ^ name ^ pos)
-end
+fun error_msg bind str =
+  let
+    val name = Binding.name_of bind
+    val pos = Position.str_of (Binding.pos_of bind)
+  in
+    error ("Head of quotient_definition " ^
+      quote str ^ " differs from declaration " ^ name ^ pos)
+  end
 
 fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
-let
-  val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
-  val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
-  val _ = if is_Const rhs then () else warning "The definiens is not a constant"
-  
-  fun sanity_test NONE _ = true
-    | sanity_test (SOME bind) str =
-        if Name.of_binding bind = str then true
-        else error_msg bind str
+  let
+    val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
+    val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
+    val _ = if is_Const rhs then () else warning "The definiens is not a constant"
 
-  val _ = sanity_test optbind lhs_str
+    fun sanity_test NONE _ = true
+      | sanity_test (SOME bind) str =
+          if Name.of_binding bind = str then true
+          else error_msg bind str
+
+    val _ = sanity_test optbind lhs_str
 
-  val qconst_bname = Binding.name lhs_str
-  val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
-  val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
-  val (_, prop') = Local_Defs.cert_def lthy prop
-  val (_, newrhs) = Local_Defs.abs_def prop'
+    val qconst_bname = Binding.name lhs_str
+    val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
+    val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
+    val (_, prop') = Local_Defs.cert_def lthy prop
+    val (_, newrhs) = Local_Defs.abs_def prop'
 
-  val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
+    val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
 
-  (* data storage *)
-  val qconst_data = {qconst = trm, rconst = rhs, def = thm}
+    (* data storage *)
+    val qconst_data = {qconst = trm, rconst = rhs, def = thm}
 
-  fun qcinfo phi = transform_qconsts phi qconst_data
-  fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
-  val lthy'' = Local_Theory.declaration true
-                 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
-in
-  (qconst_data, lthy'')
-end
+    fun qcinfo phi = transform_qconsts phi qconst_data
+    fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
+    val lthy'' = Local_Theory.declaration true
+                   (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
+  in
+    (qconst_data, lthy'')
+  end
 
 fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =
-let
-  val lhs = Syntax.read_term lthy lhs_str
-  val rhs = Syntax.read_term lthy rhs_str
-  val lthy' = Variable.declare_term lhs lthy
-  val lthy'' = Variable.declare_term rhs lthy'
-in
-  quotient_def (decl, (attr, (lhs, rhs))) lthy''
-end
+  let
+    val lhs = Syntax.read_term lthy lhs_str
+    val rhs = Syntax.read_term lthy rhs_str
+    val lthy' = Variable.declare_term lhs lthy
+    val lthy'' = Variable.declare_term rhs lthy'
+  in
+    quotient_def (decl, (attr, (lhs, rhs))) lthy''
+  end
 
 (* a wrapper for automatically lifting a raw constant *)
 fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
-let
-  val rty = fastype_of rconst
-  val qty = derive_qtyp ctxt qtys rty
-  val lhs = Free (qconst_name, qty)
-in
-  quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
-end
+  let
+    val rty = fastype_of rconst
+    val qty = derive_qtyp ctxt qtys rty
+    val lhs = Free (qconst_name, qty)
+  in
+    quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
+  end
 
 (* parser and command *)
 val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where"
 
 val quotdef_parser =
-  Scan.optional quotdef_decl (NONE, NoSyn) -- 
+  Scan.optional quotdef_decl (NONE, NoSyn) --
     Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
 
 val _ =