# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256401058 -7200
# Node ID fcacca9588b4bbb184a9d9c1c345229a83dae01a
# Parent  b1247c98abb8c3448a24d2a6042cb98cfdfa08bf
changed the definitions of liftet constants to use fun_maps

diff -r b1247c98abb8 -r fcacca9588b4 FSet.thy
--- a/FSet.thy	Sat Oct 24 17:29:20 2009 +0200
+++ b/FSet.thy	Sat Oct 24 18:17:38 2009 +0200
@@ -2,42 +2,6 @@
 imports QuotMain
 begin
 
-(* test for get_fun *)
-datatype t =
-   vr "string"
- | ap "t list"
- | lm "string" "t"
-
-consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
-axioms t_eq: "EQUIV Rt"
-
-quotient qt = "t" / "Rt"
-    by (rule t_eq)
-
-ML {*
-get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
- |> fst
- |> Syntax.string_of_term @{context}
- |> writeln
-*}
-
-ML {*
-get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}
- |> fst
- |> Syntax.string_of_term @{context}
- |> writeln
-*}
-
-ML {*
-get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
- |> fst
- |> Syntax.pretty_term @{context}
- |> Pretty.string_of
- |> writeln
-*}
-(* end test get_fun *)
-
-
 inductive
   list_eq (infix "\<approx>" 50)
 where
diff -r b1247c98abb8 -r fcacca9588b4 QuotMain.thy
--- a/QuotMain.thy	Sat Oct 24 17:29:20 2009 +0200
+++ b/QuotMain.thy	Sat Oct 24 18:17:38 2009 +0200
@@ -243,6 +243,7 @@
 end
 *}
 
+
 text {* produces the definition for a lifted constant *}
 
 ML {*
@@ -258,11 +259,12 @@
   val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys
   val abs_fn  = (fst o get_fun absF rty qty lthy) res_ty
 
+  fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2
+
+  val fns = Library.foldr (mk_fun_map) (rep_fns, abs_fn)
+            |> Syntax.check_term lthy
 in
-  map (op $) (rep_fns ~~ fresh_args)
-  |> curry list_comb oconst
-  |> curry (op $) abs_fn
-  |> fold_rev lambda fresh_args
+  fns $ oconst
 end
 *}
 
diff -r b1247c98abb8 -r fcacca9588b4 QuotTest.thy
--- a/QuotTest.thy	Sat Oct 24 17:29:20 2009 +0200
+++ b/QuotTest.thy	Sat Oct 24 18:17:38 2009 +0200
@@ -72,7 +72,6 @@
 quotient qt = "t" / "Rt"
   by (rule t_eq)
 
-
 ML {*
   get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
   |> fst