--- a/IntEx.thy	Fri Nov 27 02:23:49 2009 +0100
+++ b/IntEx.thy	Fri Nov 27 02:35:50 2009 +0100
@@ -174,7 +174,7 @@
 *)
 
 ML {*
-  mk_regularize_trm @{context} 
+  regularize_trm @{context} 
     @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"}
     @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"}
   |> Syntax.string_of_term @{context}
@@ -182,11 +182,10 @@
 *}
 
 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
-apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *})
-apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
+apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] rel_refl 1 *})
 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
-apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *})
-done 
+oops
 
 
 (*

--- a/quotient_info.ML	Fri Nov 27 02:23:49 2009 +0100
+++ b/quotient_info.ML	Fri Nov 27 02:35:50 2009 +0100
@@ -12,11 +12,6 @@
   val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
 
-  (*FIXME: obsolete *)
-  type qenv = (typ * typ) list
-  val mk_qenv: Proof.context -> qenv
-  val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option
-
   type qconsts_info = {qconst: term, rconst: term}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
   val qconsts_lookup: theory -> string -> qconsts_info option
@@ -116,22 +111,6 @@
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
 
 
-(* FIXME: obsolete: environments for quotient and raw types *)
-type qenv = (typ * typ) list
-
-fun mk_qenv ctxt =
-let
-  val thy = ProofContext.theory_of ctxt
-  val qinfo = (QuotData.get thy) |> Symtab.dest |> map snd
-in
-  map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) qinfo
-end
-
-fun lookup_qenv _ [] _ = NONE
-  | lookup_qenv eq ((qty, rty)::xs) qty' =
-      if eq (qty', qty) then SOME (qty, rty)
-      else lookup_qenv eq xs qty'
-
 (* information about quotient constants *)
 type qconsts_info = {qconst: term, rconst: term}