# HG changeset patch
# User wenzelm
# Date 1272893695 -7200
# Node ID f3157c288aca7e8505789b3fb90707220ba44597
# Parent  af4d68eccf633612f778400207447afe0cb9459e
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;

diff -r af4d68eccf63 -r f3157c288aca src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon May 03 14:38:18 2010 +0200
+++ b/src/Pure/goal.ML	Mon May 03 15:34:55 2010 +0200
@@ -137,7 +137,8 @@
         Thm.adjust_maxidx_thm ~1 #>
         Drule.implies_intr_list assms #>
         Drule.forall_intr_list fixes #>
-        Thm.generalize (map #1 tfrees, []) 0);
+        Thm.generalize (map #1 tfrees, []) 0 #>
+        Thm.strip_shyps);
     val local_result =
       Thm.future global_result global_prop
       |> Thm.instantiate (instT, [])
diff -r af4d68eccf63 -r f3157c288aca src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon May 03 14:38:18 2010 +0200
+++ b/src/Pure/thm.ML	Mon May 03 15:34:55 2010 +0200
@@ -565,14 +565,13 @@
 
 (* future rule *)
 
-fun future_result i orig_thy orig_shyps orig_prop raw_thm =
+fun future_result i orig_thy orig_shyps orig_prop thm =
   let
+    fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
+    val Thm (Deriv {promises, ...}, {thy_ref, shyps, hyps, tpairs, prop, ...}) = thm;
+
+    val _ = Theory.eq_thy (Theory.deref thy_ref, orig_thy) orelse err "bad theory";
     val _ = Theory.check_thy orig_thy;
-    val thm = strip_shyps (transfer orig_thy raw_thm);
-    val _ = Theory.check_thy orig_thy;
-    fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
-
-    val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
     val _ = prop aconv orig_prop orelse err "bad prop";
     val _ = null tpairs orelse err "bad tpairs";
     val _ = null hyps orelse err "bad hyps";