--- a/Quot/Examples/LarryInt.thy	Fri Dec 25 00:58:06 2009 +0100
+++ b/Quot/Examples/LarryInt.thy	Sat Dec 26 07:15:30 2009 +0100
@@ -2,7 +2,7 @@
 header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
 
 theory LarryInt 
-imports Nat "../QuotMain"
+imports Nat "../QuotMain" "../QuotProd"
 begin
 
 fun
@@ -361,22 +361,6 @@
 apply(auto iff: nat_raw_def)
 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_raw)