--- a/Attic/Quot/quotient_def.ML	Sun Mar 14 11:36:15 2010 +0100
+++ b/Attic/Quot/quotient_def.ML	Mon Mar 15 06:11:35 2010 +0100
@@ -1,8 +1,7 @@
-(*  Title:      quotient_def.thy
+(*  Title:      HOL/Tools/Quotient/quotient_def.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Definitions for constants on quotient types.
-
+Definitions for constants on quotient types.
 *)
 
 signature QUOTIENT_DEF =

--- a/Attic/Quot/quotient_info.ML	Sun Mar 14 11:36:15 2010 +0100
+++ b/Attic/Quot/quotient_info.ML	Mon Mar 15 06:11:35 2010 +0100
@@ -1,11 +1,9 @@
-(*  Title:      quotient_info.thy
+(*  Title:      HOL/Tools/Quotient/quotient_info.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Data slots for the quotient package.
-
+Data slots for the quotient package.
 *)
 
-
 signature QUOTIENT_INFO =
 sig
   exception NotFound
@@ -61,7 +59,7 @@
   (type T = maps_info Symtab.table
    val empty = Symtab.empty
    val extend = I
-   val merge = Symtab.merge (K true))
+   fun merge data = Symtab.merge (K true) data)
 
 fun maps_defined thy s =
   Symtab.defined (MapsData.get thy) s
@@ -125,7 +123,7 @@
   (type T = quotdata_info Symtab.table
    val empty = Symtab.empty
    val extend = I
-   val merge = Symtab.merge (K true))
+   fun merge data = Symtab.merge (K true) data)
 
 fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
   {qtyp = Morphism.typ phi qtyp,
@@ -195,7 +193,7 @@
 fun qconsts_lookup thy t =
   let
     val (name, qty) = dest_Const t
-    fun matches x =
+    fun matches (x: qconsts_info) =
       let
         val (name', qty') = dest_Const (#qconst x);
       in
@@ -284,10 +282,9 @@
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
 
 val _ = map improper_command
-  [(print_mapsinfo, "print_maps", "prints out all map functions"),
+  [(print_mapsinfo, "print_quotmaps", "prints out all map functions"),
    (print_quotinfo, "print_quotients", "prints out all quotients"),
    (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]
 
 
 end; (* structure *)
-

--- a/Attic/Quot/quotient_tacs.ML	Sun Mar 14 11:36:15 2010 +0100
+++ b/Attic/Quot/quotient_tacs.ML	Mon Mar 15 06:11:35 2010 +0100
@@ -1,8 +1,8 @@
-(*  Title:      quotient_tacs.thy
+(*  Title:      HOL/Tools/Quotient/quotient_tacs.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Tactics for solving goal arising from lifting
-    theorems to quotient types.
+Tactics for solving goal arising from lifting theorems to quotient
+types.
 *)
 
 signature QUOTIENT_TACS =
@@ -89,7 +89,7 @@
 fun get_match_inst thy pat trm =
 let
   val univ = Unify.matchers thy [(pat, trm)]
-  val SOME (env, _) = Seq.pull univ             (* raises BIND, if no unifier *)
+  val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *)  (* FIXME fragile *)
   val tenv = Vartab.dest (Envir.term_env env)
   val tyenv = Vartab.dest (Envir.type_env env)
 in

--- a/Attic/Quot/quotient_term.ML	Sun Mar 14 11:36:15 2010 +0100
+++ b/Attic/Quot/quotient_term.ML	Mon Mar 15 06:11:35 2010 +0100
@@ -1,8 +1,8 @@
-(*  Title:      quotient_term.thy
+(*  Title:      HOL/Tools/Quotient/quotient_term.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Constructs terms corresponding to goals from
-    lifting theorems to quotient types.
+Constructs terms corresponding to goals from lifting theorems to
+quotient types.
 *)
 
 signature QUOTIENT_TERM =
@@ -265,7 +265,7 @@
   | is_eq _ = false
 
 fun mk_rel_compose (trm1, trm2) =
-  Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2
+  Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
 
 fun get_relmap ctxt s =
 let
@@ -779,8 +779,4 @@
   lift_aux t
 end
 
-
 end; (* structure *)
-
-
-

--- 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 *)

--- a/Nominal/nominal_atoms.ML	Sun Mar 14 11:36:15 2010 +0100
+++ b/Nominal/nominal_atoms.ML	Mon Mar 15 06:11:35 2010 +0100
@@ -44,7 +44,7 @@
     val set = atom_decl_set str;
     val tac = rtac @{thm exists_eq_simple_sort} 1;
     val ((full_tname, info as {type_definition, Rep_name, Abs_name, ...}), thy) =
-      Typedef.add_typedef false NONE (name, [], NoSyn) set NONE tac thy;
+      Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy;
 
     (* definition of atom and permute *)
     val newT = #abs_type info;