# HG changeset patch
# User krauss
# Date 1175964870 -7200
# Node ID 1f017e6a0395361c821cdce868bdaeebc7c830dc
# Parent  0e008e3ddb1e5c4b43a43d37421f380aa8ee5721
removed obsolete workarounds

diff -r 0e008e3ddb1e -r 1f017e6a0395 src/HOL/Tools/function_package/inductive_wrap.ML
--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Sat Apr 07 12:40:32 2007 +0200
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Sat Apr 07 18:54:30 2007 +0200
@@ -52,25 +52,17 @@
                                            [] (* no special monos *)
                                            lthy
 
-      val thy = ProofContext.theory_of lthy
-                
       fun inst qdef intr_gen =
           intr_gen
-            |> Thm.freezeT
             |> requantify lthy (R, T) qdef 
           
       val intrs = map2 inst qdefs intrs_gen
                   
       val elim = elim_gen
-                   |> Thm.freezeT
                    |> forall_intr_vars (* FIXME... *)
 
-      val Rdef_real = prop_of (Thm.freezeT elim_gen)
-                       |> Logic.dest_implies |> fst
-                       |> Term.strip_comb |> snd |> hd (* Trueprop *)
-                       |> Term.strip_comb |> fst
     in
-      (intrs, (Rdef_real, elim, induct, lthy))
+      (intrs, (Rdef, elim, induct, lthy))
     end
     
 end