# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259080531 -3600
# Node ID 577539640a47133ed315f2a61593729ee43e61d5
# Parent  c5c49d240cdeca36b9df281701aa8c3a41adb1f4
merged

diff -r c5c49d240cde -r 577539640a47 QuotMain.thy
--- a/QuotMain.thy	Tue Nov 24 17:00:53 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 17:35:31 2009 +0100
@@ -6,6 +6,57 @@
 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"