--- a/Attic/Quot/quotient_typ.ML	Sun Mar 14 11:36:15 2010 +0100
+++ b/Attic/Quot/quotient_typ.ML	Mon Mar 15 06:11:35 2010 +0100
@@ -7,6 +7,9 @@
 
 signature QUOTIENT_TYPE =
 sig
+  val add_quotient_type: ((string list * binding * mixfix) * (typ * term)) * thm
+    -> Proof.context -> (thm * thm) * local_theory
+
   val quotient_type: ((string list * binding * mixfix) * (typ * term)) list
     -> Proof.context -> Proof.state
 
@@ -69,12 +72,13 @@
 fun typedef_make (vs, qty_name, mx, rel, rty) lthy =
 let
   val typedef_tac =
-     EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
+    EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
 in
-  Typedef.add_typedef false NONE
-       (qty_name, vs, mx)
-          (typedef_term rel rty lthy)
-             NONE typedef_tac lthy
+  Local_Theory.theory_result
+  (Typedef.add_typedef_global false NONE
+    (qty_name, vs, mx)
+      (typedef_term rel rty lthy)
+        NONE typedef_tac) lthy
 end
 
 
@@ -127,7 +131,7 @@
 
 
 (* main function for constructing a quotient type *)
-fun mk_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy =
+fun add_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy =
 let
   (* generates the typedef *)
   val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy
@@ -263,7 +267,7 @@
   val goals = map (mk_goal o snd) quot_list
 
   fun after_qed thms lthy =
-    fold_map mk_quotient_type (quot_list ~~ thms) lthy |> snd
+    fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd
 in
   theorem after_qed goals lthy
 end
@@ -272,14 +276,13 @@
 let
   fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy =
   let
-    (* new parsing with proper declaration *)
     val rty = Syntax.read_typ lthy rty_str
     val lthy1 = Variable.declare_typ rty lthy
     val rel = 
       Syntax.parse_term lthy1 rel_str
       |> Syntax.type_constraint (rty --> rty --> @{typ bool}) 
       |> Syntax.check_term lthy1 
-    val lthy2 = Variable.declare_term rel lthy1
+    val lthy2 = Variable.declare_term rel lthy1 
   in
     (((vs, qty_name, mx), (rty, rel)), lthy2)
   end
@@ -289,20 +292,17 @@
   quotient_type spec' lthy'
 end
 
-local
-  structure P = OuterParse;
-in
-
 val quotspec_parser =
-  P.and_list1 ((P.type_args -- P.binding) -- P.opt_infix -- 
-    (P.$$$ "=" |-- P.typ) -- (P.$$$ "/" |-- P.term))
-end
+    OuterParse.and_list1
+     ((OuterParse.type_args -- OuterParse.binding) --
+        OuterParse.opt_mixfix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
+         (OuterParse.$$$ "/" |-- OuterParse.term))
 
 val _ = OuterKeyword.keyword "/"
 
 val _ =
-  OuterSyntax.local_theory_to_proof "quotient_type"
-    "quotient type definitions (require equivalence proofs)"
-       OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
+    OuterSyntax.local_theory_to_proof "quotient_type"
+      "quotient type definitions (require equivalence proofs)"
+         OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
 
 end; (* structure *)