# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256690925 -3600
# Node ID ca9eae5bd871b462142f7776f5d67f406fb0a0b0
# Parent  2a803a1556d54838da43961b28e3025995fde75c
added a function for matching types

diff -r 2a803a1556d5 -r ca9eae5bd871 FSet.thy
--- a/FSet.thy	Tue Oct 27 14:46:38 2009 +0100
+++ b/FSet.thy	Wed Oct 28 01:48:45 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 2a803a1556d5 -r ca9eae5bd871 QuotMain.thy
--- 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)
 *}