# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1255383554 -7200
# Node ID c8d58e2cda58e691658016e2ce2baaf92d3236e2
# Parent  3a68c1693a32fbb0e282f5562a994833dd056362
slightly modified the parser

diff -r 3a68c1693a32 -r c8d58e2cda58 QuotMain.thy
--- a/QuotMain.thy	Mon Oct 12 23:16:20 2009 +0200
+++ b/QuotMain.thy	Mon Oct 12 23:39:14 2009 +0200
@@ -166,7 +166,7 @@
 where
   r_eq: "EQUIV RR"
 
-quotient qtrm = "trm" / "RR"
+quotient qtrm = trm / "RR"
   apply(rule r_eq)
   done
 
@@ -196,7 +196,7 @@
 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
 axioms r_eq': "EQUIV R'"
 
-quotient "'a qtrm'" = "'a trm'" / "R'"
+quotient qtrm' = "'a trm'" / "R'"
   apply(rule r_eq')
   done
 
@@ -218,7 +218,7 @@
 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
 axioms t_eq: "EQUIV Rt"
 
-quotient "qt" = "t" / "Rt"
+quotient qt = "t" / "Rt"
   by (rule t_eq)
 
 section {* lifting of constants *}
@@ -408,7 +408,7 @@
 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
 axioms t_eq': "EQUIV Rt'"
 
-quotient "'a qt'" = "'a t'" / "Rt'"
+quotient qt' = "'a t'" / "Rt'"
   apply(rule t_eq')
   done
 
@@ -453,7 +453,7 @@
   apply(auto intro: list_eq.intros list_eq_refl)
   done
 
-quotient "'a fset" = "'a list" / "list_eq"
+quotient fset = "'a list" / "list_eq"
   apply(rule equiv_list_eq)
   done
 
diff -r 3a68c1693a32 -r c8d58e2cda58 quotient.ML
--- a/quotient.ML	Mon Oct 12 23:16:20 2009 +0200
+++ b/quotient.ML	Mon Oct 12 23:39:14 2009 +0200
@@ -163,10 +163,8 @@
 (* syntax setup *)
 local structure P = OuterParse in
 
-fun mk_typedef (qty, mx, rty, rel_trm) lthy = 
+fun mk_typedef (qty_name, mx, rty, rel_trm) lthy = 
 let
-  val (qty_name, _) = Term.dest_Type qty 
-
   val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   val EQUIV_goal = HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel_trm)
 		    
@@ -181,18 +179,17 @@
 end
 
 val quottype_parser = 
-    P.typ -- P.opt_infix -- 
+    P.short_ident -- P.opt_infix -- 
        (P.$$$ "=" |-- P.typ) -- 
          (P.$$$ "/" |-- P.term)
            
 fun mk_typedef_cmd (((qstr, mx), rstr), rel_str) lthy = 
 let
-  val qty = Syntax.parse_typ lthy qstr
   val rty = Syntax.parse_typ lthy rstr
   val rel_trm = Syntax.parse_term lthy rel_str
                 |> Syntax.check_term lthy
 in
-  mk_typedef (qty, mx, rty, rel_trm) lthy  
+  mk_typedef (qstr, mx, rty, rel_trm) lthy  
 end
 
 val _ = OuterKeyword.keyword "/"