--- a/QuotMain.thy	Wed Dec 02 20:54:59 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 23:11:50 2009 +0100
@@ -5,59 +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 make_inst lhs t =
-  let
-    val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
-    val _ $ (Abs (_, _, g)) = t;
-    
-  fun mk_abs i t =
-      if incr_boundvars i u aconv t then Bound i
-      else (case t of
-        t1 $ t2 => mk_abs i t1 $ mk_abs i t2
-      | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
-      | Bound j => if i = j then error "make_inst" else t
-      | _ => t);
-
-  in (f, Abs ("x", T, mk_abs 0 g)) end;
-*}
-
-ML {* 
-  val trm1 = @{term_pat "(P::(nat\<Rightarrow>bool)\<Rightarrow>bool) (\<lambda>(x::nat). (?f ((g::nat\<Rightarrow>nat) x)))"}; 
-  val trm2 = @{term_pat "(P::(nat\<Rightarrow>bool)\<Rightarrow>bool) (\<lambda>(x::nat). (h (g x) ((g::nat\<Rightarrow>nat) x)))"}
-*}
-
-ML {*
-fun test trm =
-  case trm of
-  (_ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u))) => (1,f)
-  | (_ $ (Abs (_, _, (f as (Var (_, _)) $ u)))) => (2,f)
-  | (_ $ (Abs (_, _, (f $ u)))) => (3,f)
-*}
-
-ML {* test trm1 *}
-
-ML {*
- make_inst trm1 trm2
-  |> pairself (Syntax.string_of_term @{context})
-  |> pairself writeln
-*}
-
-
-
-
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"