--- 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