# 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