# HG changeset patch # User obua # Date 1126555627 -7200 # Node ID 7bbfb79eda96fef173b32019180245387b020512 # Parent 9008633b237e55522b165c1a1823bbc5eab96c04 removed clutter diff -r 9008633b237e -r 7bbfb79eda96 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Mon Sep 12 20:31:56 2005 +0200 +++ b/src/HOL/Import/proof_kernel.ML Mon Sep 12 22:07:07 2005 +0200 @@ -123,6 +123,7 @@ fun hthm2thm (HOLThm (_, th)) = th + datatype proof_info = Info of {disk_info: (string * string) option ref} @@ -1019,46 +1020,6 @@ th |> forall_intr_list dom |> forall_elim_list rng -fun apply_tyinst_typ tyinst = - let - fun G (ty as TFree _) = - (case try (Lib.assoc ty) tyinst of - SOME ty' => ty' - | NONE => ty) - | G (Type(tyname,tys)) = Type(tyname,map G tys) - | G (TVar _) = raise ERR "apply_tyinst_typ" "Scematic variable found" - in - G - end - -fun apply_tyinst_term tyinst = - let - val G = apply_tyinst_typ tyinst - fun F (tm as Bound _) = tm - | F (tm as Free(vname,ty)) = Free(vname,G ty) - | F (tm as Const(vname,ty)) = Const(vname,G ty) - | F (tm1 $ tm2) = (F tm1) $ (F tm2) - | F (Abs(vname,ty,body)) = Abs(vname,G ty,F body) - | F (Var _) = raise ERR "apply_tyinst_term" "Schematic variable found" - in - F - end - -fun apply_inst_term tminst = - let - fun F (tm as Bound _) = tm - | F (tm as Free _) = - (case try (Lib.assoc tm) tminst of - SOME tm' => tm' - | NONE => tm) - | F (tm as Const _) = tm - | F (tm1 $ tm2) = (F tm1) $ (F tm2) - | F (Abs(vname,ty,body)) = Abs(vname,ty,F body) - | F (Var _) = raise ERR "apply_inst_term" "Schematic variable found" - in - F - end - val collect_vars = let fun F vars (Bound _) = vars @@ -1354,8 +1315,7 @@ )) (zip tys_before tys_after) val res = Drule.instantiate (tyinst,[]) th1 - val appty = apboth (apply_tyinst_term lambda) - val hth = HOLThm(map appty rens,res) + val hth = HOLThm([],res) val res = norm_hthm sg hth val _ = message "RESULT:" val _ = if_debug pth res @@ -1370,12 +1330,9 @@ val _ = if_debug pth hth val sg = sign_of thy val (sdom,srng) = ListPair.unzip sigma - val (info,th) = disamb_thm hth - val (info',srng') = disamb_terms_from info srng - val rens = rens_of info' - val sdom' = map (apply_inst_term rens) sdom - val th1 = mk_INST (map (cterm_of sg) sdom') (map (cterm_of sg) srng') th - val res = HOLThm(rens,th1) + val th = hthm2thm hth + val th1 = mk_INST (map (cterm_of sg) sdom) (map (cterm_of sg) srng) th + val res = HOLThm([],th1) val _ = message "RESULT:" val _ = if_debug pth res in