--- a/QuotMain.thy	Thu Nov 26 21:01:53 2009 +0100
+++ b/QuotMain.thy	Thu Nov 26 21:04:17 2009 +0100
@@ -902,127 +902,6 @@
 
 section {* Cleaning of the theorem *}
 
-(* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
-ML {*
-fun exchange_ty lthy rty qty ty =
-  let
-    val thy = ProofContext.theory_of lthy
-  in
-    if Sign.typ_instance thy (ty, rty) then
-      let
-        val inst = Sign.typ_match thy (rty, ty) Vartab.empty
-      in
-        Envir.subst_type inst qty
-      end
-    else
-      let
-        val (s, tys) = dest_Type ty
-      in
-        Type (s, map (exchange_ty lthy rty qty) tys)
-      end
-  end
-  handle TYPE _ => ty (* for dest_Type *)
-*}
-
-
-ML {*
-fun find_matching_types rty ty =
-  if Type.raw_instance (Logic.varifyT ty, rty)
-  then [ty]
-  else
-    let val (s, tys) = dest_Type ty in
-    flat (map (find_matching_types rty) tys)
-    end
-    handle TYPE _ => []
-*}
-
-ML {*
-fun negF absF = repF
-  | negF repF = absF
-
-fun get_fun flag qenv lthy ty =
-let
-  
-  fun get_fun_aux s fs =
-   (case (maps_lookup (ProofContext.theory_of lthy) s) of
-      SOME info => list_comb (Const (#mapfun info, dummyT), fs)
-    | NONE      => error ("no map association for type " ^ s))
-
-  fun get_const flag qty =
-  let 
-    val thy = ProofContext.theory_of lthy
-    val qty_name = Long_Name.base_name (fst (dest_Type qty))
-  in
-    case flag of
-      absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)
-    | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
-  end
-
-  fun mk_identity ty = Abs ("", ty, Bound 0)
-
-in
-  if (AList.defined (op=) qenv ty)
-  then (get_const flag ty)
-  else (case ty of
-          TFree _ => mk_identity ty
-        | Type (_, []) => mk_identity ty 
-        | Type ("fun" , [ty1, ty2]) => 
-            let
-              val fs_ty1 = get_fun (negF flag) qenv lthy ty1
-              val fs_ty2 = get_fun flag qenv lthy ty2
-            in  
-              get_fun_aux "fun" [fs_ty1, fs_ty2]
-            end 
-        | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
-        | _ => error ("no type variables allowed"))
-end
-*}
-
-ML {*
-fun get_fun_OLD flag (rty, qty) lthy ty =
-  let
-    val tys = find_matching_types rty ty;
-    val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
-    val xchg_ty = exchange_ty lthy rty qty ty
-  in
-    get_fun flag qenv lthy xchg_ty
-  end
-*}
-
-ML {*
-fun applic_prs_old lthy rty qty absrep ty =
-  let
-    val rty = Logic.varifyT rty;
-    val qty = Logic.varifyT qty;
-    fun absty ty =
-      exchange_ty lthy rty qty ty
-    fun mk_rep tm =
-      let
-        val ty = exchange_ty lthy qty rty (fastype_of tm)
-      in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end;
-    fun mk_abs tm =
-      let
-        val ty = fastype_of tm
-      in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end
-    val (l, ltl) = Term.strip_type ty;
-    val nl = map absty l;
-    val vs = map (fn _ => "x") l;
-    val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
-    val args = map Free (vfs ~~ nl);
-    val lhs = list_comb((Free (fname, nl ---> ltl)), args);
-    val rargs = map mk_rep args;
-    val f = Free (fname, nl ---> ltl);
-    val rhs = mk_abs (list_comb((mk_rep f), rargs));
-    val eq = Logic.mk_equals (rhs, lhs);
-    val ceq = cterm_of (ProofContext.theory_of lthy') eq;
-    val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps});
-    val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
-    val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;
-  in
-    singleton (ProofContext.export lthy' lthy) t_id
-  end
-*}
-
 ML {*
 fun applic_prs lthy absrep (rty, qty) =
   let