src/Pure/tctical.ML

   DOES NOT work if tactic affects the main goal other than by instantiation.*)
 
 (*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_of ProtoPure.thy) 
+val prop_equals = cterm_of (Theory.sign_of ProtoPure.thy) 
                     (Const("==", propT-->propT-->propT));
 
 fun mk_prop_equals(t,u) = capply (capply prop_equals t) u;
 
 (*Like trivial but returns [ct==X] ct==>X instead of ct==>ct, if possible.
   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_of ProtoPure.thy)
+  let val xfree = cterm_of (Theory.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 = 
           implies_elim 

 	  eq_trivial (adjust_maxidx (List.nth(cprems_of st, i-1)))
       fun next st' = 
 	  let val np' = nprems_of st'
               (*rename the ?A in rev_triv_goal*)
 	      val {maxidx,...} = rep_thm st'
-              val ct = cterm_of (sign_of ProtoPure.thy)
+              val ct = cterm_of (Theory.sign_of ProtoPure.thy)
 		                (Var(("A",maxidx+1), propT))
 	      val rev_triv_goal' = instantiate' [] [Some ct] Drule.rev_triv_goal
               fun bic th = bicompose false (false, th, np')
           in  bic (Seq.hd (bic (restore st') 1 rev_triv_goal')) i st  end 
   in  Seq.flat (Seq.map next (tac eq_cprem))