# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256690971 -3600
# Node ID 7610d2bbca48803186d4de5947314cea7c86d951
# Parent  ca9eae5bd871b462142f7776f5d67f406fb0a0b0# Parent  80859cc80332dd99144f175b91b3e241d374e887
merged

diff -r 80859cc80332 -r 7610d2bbca48 FSet.thy
--- a/FSet.thy	Tue Oct 27 18:05:45 2009 +0100
+++ b/FSet.thy	Wed Oct 28 01:49:31 2009 +0100
@@ -168,7 +168,8 @@
 thm fold_def
 
 local_setup {*
-  make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+  make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn 
+  @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
 term map
@@ -176,6 +177,8 @@
 thm fmap_def
 
 
+
+
 ML {*
   val consts = [@{const_name "Nil"}, @{const_name "Cons"},
                 @{const_name "membship"}, @{const_name "card1"},
diff -r 80859cc80332 -r 7610d2bbca48 QuotMain.thy
--- a/QuotMain.thy	Tue Oct 27 18:05:45 2009 +0100
+++ b/QuotMain.thy	Wed Oct 28 01:49:31 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)
 *}