# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256651198 -3600
# Node ID 2a803a1556d54838da43961b28e3025995fde75c
# Parent  524e0e9cf6b61f35734f4dc2e2a8cf1ea876854b
tuned

diff -r 524e0e9cf6b6 -r 2a803a1556d5 QuotMain.thy
--- a/QuotMain.thy	Tue Oct 27 14:15:40 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 14:46:38 2009 +0100
@@ -152,7 +152,7 @@
 ML {*
 val quot_def_parser = 
   (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- 
-    ((OuterParse.list1 OuterParse.binding) --| OuterParse.$$$ ")")) --
+    ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) --
       (OuterParse.binding -- 
         Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- 
          OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec)
diff -r 524e0e9cf6b6 -r 2a803a1556d5 quotient.ML
--- a/quotient.ML	Tue Oct 27 14:15:40 2009 +0100
+++ b/quotient.ML	Tue Oct 27 14:46:38 2009 +0100
@@ -103,7 +103,7 @@
 
 
 
-(* wrappers for define, note and theorem_i*)
+(* wrappers for define, note and theorem_i *)
 fun define (name, mx, rhs) lthy =
 let
   val ((rhs, (_ , thm)), lthy') =
@@ -163,7 +163,7 @@
 (* tactic to prove the QUOT_TYPE theorem for the new type *)
 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
 let
-  val unfold_mem = MetaSimplifier.rewrite_rule @{thms mem_def}
+  val unfold_mem = MetaSimplifier.rewrite_rule [@{thm mem_def}]
   val rep_thm = #Rep typedef_info |> unfold_mem
   val rep_inv = #Rep_inverse typedef_info
   val abs_inv = #Abs_inverse typedef_info |> unfold_mem
@@ -300,27 +300,26 @@
 in
   theorem after_qed goals lthy
 end
+           
+fun mk_quotient_type_cmd spec lthy = 
+let
+  fun parse_spec (((qty_str, mx), rty_str), rel_str) =
+  let
+    val qty_name = Binding.name qty_str
+    val rty = Syntax.parse_typ lthy rty_str |> Syntax.check_typ lthy
+    val rel = Syntax.parse_term lthy rel_str |> Syntax.check_term lthy
+  in
+    ((qty_name, mx), (rty, rel))
+  end
+in
+  mk_quotient_type (map parse_spec spec) lthy
+end
 
 val quotspec_parser = 
     OuterParse.and_list1
      (OuterParse.short_ident -- OuterParse.opt_infix -- 
        (OuterParse.$$$ "=" |-- OuterParse.typ) -- 
          (OuterParse.$$$ "/" |-- OuterParse.term))
-           
-fun mk_quotient_type_cmd spec lthy = 
-let
-  fun parse_spec (((qty_str, mx), rty_str), rel_str) =
-  let
-    val qty_name = Binding.name qty_str
-    val rty = Syntax.parse_typ lthy rty_str
-    val rel = Syntax.parse_term lthy rel_str
-              |> Syntax.check_term lthy
-  in
-    ((qty_name, mx), (rty, rel))
-  end
-in
-  mk_quotient_type (map parse_spec spec) lthy
-end
 
 val _ = OuterKeyword.keyword "/"