src/Pure/tactic.ML
changeset 6390 5d58c100ca3f
parent 5974 6acf3ff0f486
child 6964 0c894ad53457
     1.1 --- a/src/Pure/tactic.ML	Wed Mar 17 16:32:38 1999 +0100
     1.2 +++ b/src/Pure/tactic.ML	Wed Mar 17 16:33:00 1999 +0100
     1.3 @@ -293,7 +293,7 @@
     1.4    increment revcut_rl instead.*)
     1.5  fun make_elim_preserve rl = 
     1.6    let val {maxidx,...} = rep_thm rl
     1.7 -      fun cvar ixn = cterm_of (sign_of ProtoPure.thy) (Var(ixn,propT));
     1.8 +      fun cvar ixn = cterm_of (Theory.sign_of ProtoPure.thy) (Var(ixn,propT));
     1.9        val revcut_rl' = 
    1.10  	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
    1.11  			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl