--- a/Quot/Examples/LarryInt.thy	Fri Dec 11 15:58:15 2009 +0100
+++ b/Quot/Examples/LarryInt.thy	Fri Dec 11 17:03:34 2009 +0100
@@ -382,10 +382,9 @@
 
 (* PROBLEM: this has to be a definition, not an abbreviation *)
 (* otherwise the lemma nat_le_eq_zle cannot be lifted        *)
-fun
-  nat_aux
-where
-  "nat_aux (x, y) =  x - (y::nat)"
+
+abbreviation
+  "nat_aux \<equiv> \<lambda>(x, y).x - (y::nat)"
 
 quotient_def
   "nat2::int\<Rightarrow>nat"
@@ -405,12 +404,27 @@
 apply(auto)
 done
 
+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
+
+*}
+
+consts test::"'b \<Rightarrow> 'b \<Rightarrow> 'b"
+
+
 lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
 unfolding less_int_def
 apply(lifting nat_le_eq_zle_aux)
 apply(injection)
 apply(simp_all only: quot_respect)
 done
-(* PROBLEM *)
 
 end