--- a/src/Pure/Tools/rule_insts.ML Tue Mar 03 19:08:04 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML Wed Mar 04 19:53:18 2015 +0100
@@ -213,7 +213,7 @@
(* Tactic *)
fun tac i st = CSUBGOAL (fn (cgoal, _) =>
let
- val goal = term_of cgoal;
+ val goal = Thm.term_of cgoal;
val params = Logic.strip_params goal; (*params of subgoal i as string typ pairs*)
val params = rev (Term.rename_wrt_term goal params)
(*as they are printed: bound variables with*)
@@ -265,12 +265,12 @@
fun liftterm t =
fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct);
- val lifttvar = apply2 (ctyp_of thy o Logic.incr_tvar inc);
+ val lifttvar = apply2 (Thm.ctyp_of thy o Logic.incr_tvar inc);
val rule = Drule.instantiate_normalize
(map lifttvar envT', map liftpair cenv)
(Thm.lift_rule cgoal thm)
in
- compose_tac ctxt' (bires_flag, rule, nprems_of thm) i
+ compose_tac ctxt' (bires_flag, rule, Thm.nprems_of thm) i
end) i st;
in tac end;