# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256393345 -7200
# Node ID 09048a951dca292531c2b6148a228de4a36ca18a
# Parent  7cf227756e2a2fdc2982db715c241f65e0968f51
moved the map_funs setup into QuotMain

diff -r 7cf227756e2a -r 09048a951dca FSet.thy
--- a/FSet.thy	Sat Oct 24 14:00:18 2009 +0200
+++ b/FSet.thy	Sat Oct 24 16:09:05 2009 +0200
@@ -14,18 +14,11 @@
 quotient qt = "t" / "Rt"
     by (rule t_eq)
 
-setup {*
-  maps_update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #>
-  maps_update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #>
-  maps_update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
-*}
-
-
 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
+ |> writeln*)
 *}
 
 ML {*
diff -r 7cf227756e2a -r 09048a951dca QuotMain.thy
--- a/QuotMain.thy	Sat Oct 24 14:00:18 2009 +0200
+++ b/QuotMain.thy	Sat Oct 24 16:09:05 2009 +0200
@@ -158,6 +158,12 @@
 use "quotient.ML"
 
 (* mapfuns for some standard types *)
+setup {*
+  maps_update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #>
+  maps_update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #>
+  maps_update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
+*}
+
 
 ML {* quotdata_lookup @{theory} *}
 setup {* quotdata_update_thy (@{typ nat}, @{typ bool}, @{term "True"})*}