diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/quotient_typ.ML	Thu Feb 11 10:06:02 2010 +0100
@@ -7,10 +7,10 @@
 
 signature QUOTIENT_TYPE =
 sig
-  val quotient_type: ((string list * binding * mixfix) * (typ * term)) list 
+  val quotient_type: ((string list * binding * mixfix) * (typ * term)) list
     -> Proof.context -> Proof.state
 
-  val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list 
+  val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list
     -> Proof.context -> Proof.state
 end;
 
@@ -41,7 +41,7 @@
 let
   val goals' = map (rpair []) goals
   fun after_qed' thms = after_qed (the_single thms)
-in 
+in
   Proof.theorem_i NONE after_qed' [goals'] ctxt
 end
 
@@ -155,7 +155,7 @@
   (* quot_type theorem *)
   val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3
 
-  (* quotient theorem *)  
+  (* quotient theorem *)
   val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3
   val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
 
@@ -189,22 +189,22 @@
     else [qty_str ^ "illegal schematic variable(s) in the relation."]
 
   val dup_vs =
-    (case duplicates (op =) vs of 
+    (case duplicates (op =) vs of
        [] => []
      | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
 
   val extra_rty_tfrees =
-    (case subtract (op =) vs rty_tfreesT of 
+    (case subtract (op =) vs rty_tfreesT of
        [] => []
      | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
 
   val extra_rel_tfrees =
-    (case subtract (op =) vs rel_tfrees of 
+    (case subtract (op =) vs rel_tfrees of
        [] => []
      | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
- 
+
   val illegal_rel_frees =
-    (case rel_frees of 
+    (case rel_frees of
       [] => []
     | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
 
@@ -248,28 +248,28 @@
  relations are equivalence relations
 *)
 
-fun quotient_type quot_list lthy = 
+fun quotient_type quot_list lthy =
 let
-  (* sanity check *)  
-  val _ = List.app sanity_check quot_list 
+  (* sanity check *)
+  val _ = List.app sanity_check quot_list
   val _ = List.app (map_check lthy) quot_list
 
   fun mk_goal (rty, rel) =
   let
     val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
-  in 
+  in
     HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel)
   end
 
   val goals = map (mk_goal o snd) quot_list
-              
+
   fun after_qed thms lthy =
     fold_map mk_quotient_type (quot_list ~~ thms) lthy |> snd
 in
   theorem after_qed goals lthy
 end
-           
-fun quotient_type_cmd specs lthy = 
+
+fun quotient_type_cmd specs lthy =
 let
   fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy =
   let
@@ -278,12 +278,12 @@
     val lthy1 = Variable.declare_typ rty lthy
     val pre_rel = Syntax.parse_term lthy1 rel_str
     val pre_rel' = Syntax.type_constraint (rty --> rty --> @{typ bool}) pre_rel
-    val rel = Syntax.check_term lthy1 pre_rel'   
+    val rel = Syntax.check_term lthy1 pre_rel'
     val lthy2 = Variable.declare_term rel lthy1
-   
+
     (* old parsing *)
     (* val rty = Syntax.read_typ lthy rty_str
-       val rel = Syntax.read_term lthy rel_str *) 
+       val rel = Syntax.read_term lthy rel_str *)
   in
     (((vs, qty_name, mx), (rty, rel)), lthy2)
   end
@@ -293,16 +293,16 @@
   quotient_type spec' lthy'
 end
 
-val quotspec_parser = 
+val quotspec_parser =
     OuterParse.and_list1
-     ((OuterParse.type_args -- OuterParse.binding) -- 
-        OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- 
+     ((OuterParse.type_args -- OuterParse.binding) --
+        OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
          (OuterParse.$$$ "/" |-- OuterParse.term))
 
 val _ = OuterKeyword.keyword "/"
 
-val _ = 
-    OuterSyntax.local_theory_to_proof "quotient_type" 
+val _ =
+    OuterSyntax.local_theory_to_proof "quotient_type"
       "quotient type definitions (require equivalence proofs)"
          OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)