--- a/QuotMain.thy	Tue Nov 24 18:13:18 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 18:13:57 2009 +0100
@@ -5,58 +5,6 @@
      ("quotient_def.ML")
 begin
 
-
-ML {*
-let
-   val parser = Args.context -- Scan.lift Args.name_source
-   fun term_pat (ctxt, str) =
-      str |> ProofContext.read_term_pattern ctxt
-          |> ML_Syntax.print_term
-          |> ML_Syntax.atomic
-in
-   ML_Antiquote.inline "term_pat" (parser >> term_pat)
-end
-*}
-
-ML {*
-fun pretty_helper aux env =
-  env |> Vartab.dest
-      |> map ((fn (s1, s2) => s1 ^ " := " ^ s2) o aux)
-      |> commas
-      |> enclose "[" "]"
-      |> tracing
-*}
-
-ML {*
-fun pretty_env ctxt env =
-let
-   fun get_trms (v, (T, t)) = (Var (v, T), t)
-   val print = pairself (Syntax.string_of_term ctxt)
-in
-   pretty_helper (print o get_trms) env
-end
-*}
-
-ML {* val pat = @{term_pat "\<lambda>(x::'a list \<Rightarrow> bool). 
-         (?f)
-         ((g::('a list \<Rightarrow> bool)\<Rightarrow>'a list \<Rightarrow> bool) x)"} *}
-ML {* val trm = @{term_pat "\<lambda>(x::'a list \<Rightarrow> bool). 
-          (f::('a List.list \<Rightarrow> bool) \<Rightarrow> ('a List.list \<Rightarrow> bool) \<Rightarrow> 'b)
-          ((g::('a list \<Rightarrow> bool)\<Rightarrow>'a list \<Rightarrow> bool) x) ((g::('a list \<Rightarrow> bool)\<Rightarrow>'a list \<Rightarrow> bool) x)"} *}
-
-ML {* val univ = let
-  val init = Envir.empty 0
-in
-  Unify.unifiers (@{theory}, init, [(pat, trm)])
-end
-*}
-
-ML {* val SOME ((u1, _), next) = Seq.pull univ *}
-ML {* val NEXT = Seq.pull next *}
-
-ML {* show_types := true *}
-ML {* pretty_env @{context} (Envir.term_env u1); *}
-
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -1644,6 +1592,28 @@
   THEN' (quotient_tac quot);
 *}
 
+ML {* 
+fun prep_trm thy (x, (T, t)) = 
+  (cterm_of thy (Var (x, T)), cterm_of thy t) 
+
+fun prep_ty thy (x, (S, ty)) = 
+  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) 
+*}
+
+ML {*
+fun unify_prs thy pat trm = 
+let
+  val init = Envir.empty 0 (* FIXME: get the max-index *)
+  val univ = Unify.smash_unifiers thy [(pat, trm)] init
+  val SOME (env, _) = Seq.pull univ
+  val tenv = Vartab.dest (Envir.term_env env)
+  val tyenv =  Vartab.dest (Envir.type_env env)
+in
+  (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+end 
+*}
+
+
 ML {*
 fun lambda_prs_tac lthy quot =
   (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS}