# HG changeset patch # User wenzelm # Date 1213200242 -7200 # Node ID 113a32dd0b14fe33678242289d35e36fef57d6a1 # Parent 0ddb5576b3874b53f1ac5d66fd58aab22981b277 Drule.read_instantiate; Drule.types_sorts; diff -r 0ddb5576b387 -r 113a32dd0b14 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Wed Jun 11 18:03:38 2008 +0200 +++ b/src/Pure/tactic.ML Wed Jun 11 18:04:02 2008 +0200 @@ -220,11 +220,11 @@ fun read_insts_in_state (st, i, sinsts, rule) = let val thy = Thm.theory_of_thm st and params = params_of_state i st - and rts = types_sorts rule and (types,sorts) = types_sorts st + and rts = Drule.types_sorts rule and (types,sorts) = Drule.types_sorts st fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm) | types' ixn = types ixn; val used = Drule.add_used rule (Drule.add_used st []); - in read_insts thy rts (types',sorts) used sinsts end; + in Drule.read_insts thy rts (types',sorts) used sinsts end; (*Lift and instantiate a rule wrt the given state and subgoal number *) fun lift_inst_rule' (st, i, sinsts, rule) = @@ -340,7 +340,7 @@ fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); (*instantiate variables in the whole state*) -val instantiate_tac = PRIMITIVE o read_instantiate; +val instantiate_tac = PRIMITIVE o Drule.read_instantiate; val instantiate_tac' = PRIMITIVE o Drule.read_instantiate';