--- a/QuotMain.thy	Mon Nov 23 14:16:41 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 14:32:11 2009 +0100
@@ -485,66 +485,6 @@
 *}
 *)
 
-
-ML {*
-fun negF absF = repF
-  | negF repF = absF
-
-fun get_fun_noexchange flag (rty, qty) lthy ty =
-let
-  fun get_fun_aux s fs_tys =
-  let
-    val (fs, tys) = split_list fs_tys
-    val (otys, ntys) = split_list tys
-    val oty = Type (s, otys)
-    val nty = Type (s, ntys)
-    val ftys = map (op -->) tys
-  in
-   (case (maps_lookup (ProofContext.theory_of lthy) s) of
-      SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))
-    | NONE      => error ("no map association for type " ^ s))
-  end
-
-  fun get_fun_fun fs_tys =
-  let
-    val (fs, tys) = split_list fs_tys
-    val ([oty1, oty2], [nty1, nty2]) = split_list tys
-    val oty = nty1 --> oty2
-    val nty = oty1 --> nty2
-    val ftys = map (op -->) tys
-  in
-    (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
-  end
-
-  val thy = ProofContext.theory_of lthy
-
-  fun get_const flag (rty, qty) =
-  let 
-    val qty_name = Long_Name.base_name (fst (dest_Type qty))
-  in
-    case flag of
-      absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))
-    | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
-  end
-
-  fun mk_identity ty = Abs ("", ty, Bound 0)
-
-in
-  if (Sign.typ_instance thy (ty, rty))
-  then (get_const flag (ty, (exchange_ty lthy rty qty ty)))
-  else (case ty of
-          TFree _ => (mk_identity ty, (ty, ty))
-        | Type (_, []) => (mk_identity ty, (ty, ty))
-        | Type ("fun" , [ty1, ty2]) =>
-                 get_fun_fun [get_fun_noexchange (negF flag) (rty, qty) lthy ty1,
-                 get_fun_noexchange flag (rty, qty) lthy ty2]
-        | Type (s, tys) => get_fun_aux s (map (get_fun_noexchange flag (rty, qty) lthy) tys)
-        | _ => raise ERROR ("no type variables"))
-end
-fun get_fun_noex flag (rty, qty) lthy ty =
-  fst (get_fun_noexchange flag (rty, qty) lthy ty)
-*}
-
 ML {*
 fun find_matching_types rty ty =
   if Type.raw_instance (Logic.varifyT ty, rty)
@@ -622,38 +562,6 @@
   end
 *}
 
-(*
-consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
-axioms Rl_eq: "EQUIV Rl"
-
-quotient ql = "'a list" / "Rl"
-  by (rule Rl_eq)
-
-ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *}
-ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *}
-ML {* val ttt = term_of @{cterm "f :: bool list \<Rightarrow> nat list"} *}
-
-ML {*
-  get_fun_noexchange absF (al, aq) @{context} (fastype_of ttt)
-*}
-ML {*
-  get_fun_new absF al aq @{context} (fastype_of ttt)
-*}
-ML {*
-  fun mk_abs tm =
-    let
-      val ty = fastype_of tm
-    in (get_fun_noexchange absF (al, aq) @{context} ty) $ tm end
-  fun mk_repabs tm =
-    let
-      val ty = fastype_of tm
-    in (get_fun_noexchange repF (al, aq) @{context} ty) $ (mk_abs tm) end
-*}
-ML {*
-  cterm_of @{theory} (mk_repabs ttt)
-*}
-*)
-
 text {* Does the same as 'subst' in a given prop or theorem *}
 ML {*
 fun eqsubst_prop ctxt thms t =