--- a/src/Pure/tctical.ML Fri Oct 24 17:12:35 1997 +0200
+++ b/src/Pure/tctical.ML Fri Oct 24 17:13:21 1997 +0200
@@ -334,7 +334,7 @@
(*SELECT_GOAL optimization: replace the conclusion by a variable X,
to avoid copying. Proof states have X==concl as an assuption.*)
-val prop_equals = cterm_of Sign.proto_pure
+val prop_equals = cterm_of (sign_of ProtoPure.thy)
(Const("==", propT-->propT-->propT));
fun mk_prop_equals(t,u) = capply (capply prop_equals t) u;
@@ -343,7 +343,7 @@
It is paired with a function to undo the transformation. If ct contains
Vars then it returns ct==>ct.*)
fun eq_trivial ct =
- let val xfree = cterm_of Sign.proto_pure (Free (gensym"EQ_TRIVIAL_", propT))
+ let val xfree = cterm_of (sign_of ProtoPure.thy) (Free (gensym"EQ_TRIVIAL_", propT))
val ct_eq_x = mk_prop_equals (ct, xfree)
and refl_ct = reflexive ct
fun restore th =
@@ -367,7 +367,7 @@
(* (!!selct. PROP ?V) ==> PROP ?V ; contains NO TYPE VARIABLES.*)
val dummy_quant_rl =
- read_cterm Sign.proto_pure ("!!selct::prop. PROP V",propT) |>
+ read_cterm (sign_of ProtoPure.thy) ("!!selct::prop. PROP V",propT) |>
assume |> forall_elim_var 0 |> standard;
(* Prevent the subgoal's assumptions from becoming additional subgoals in the