--- a/QuotMain.thy	Tue Oct 27 14:46:38 2009 +0100
+++ b/QuotMain.thy	Wed Oct 28 01:48:45 2009 +0100
@@ -137,8 +137,6 @@
 
 section {* type definition for the quotient type *}
 
-ML {* Proof.theorem_i NONE *}
-
 use "quotient.ML"
 
 declare [[map list = (map, LIST_REL)]]
@@ -150,6 +148,13 @@
 ML {* maps_lookup @{theory} "fun" *}
 
 ML {*
+fun matches ty1 ty2 =
+  Type.raw_instance (ty1, Logic.varifyT ty2)
+*}
+
+
+
+ML {*
 val quot_def_parser = 
   (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- 
     ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) --
@@ -163,7 +168,7 @@
 *}
 
 ML {*
-val _ = OuterSyntax.local_theory "quotient_def" "lifted definition"
+val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
   OuterKeyword.thy_decl (quot_def_parser >> test)
 *}