# 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";