src/Pure/tactic.ML
changeset 27158 113a32dd0b14
parent 26626 c6231d64d264
child 27209 388fd72e9f26
     1.1 --- a/src/Pure/tactic.ML	Wed Jun 11 18:03:38 2008 +0200
     1.2 +++ b/src/Pure/tactic.ML	Wed Jun 11 18:04:02 2008 +0200
     1.3 @@ -220,11 +220,11 @@
     1.4  fun read_insts_in_state (st, i, sinsts, rule) =
     1.5    let val thy = Thm.theory_of_thm st
     1.6        and params = params_of_state i st
     1.7 -      and rts = types_sorts rule and (types,sorts) = types_sorts st
     1.8 +      and rts = Drule.types_sorts rule and (types,sorts) = Drule.types_sorts st
     1.9        fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm)
    1.10          | types' ixn = types ixn;
    1.11        val used = Drule.add_used rule (Drule.add_used st []);
    1.12 -  in read_insts thy rts (types',sorts) used sinsts end;
    1.13 +  in Drule.read_insts thy rts (types',sorts) used sinsts end;
    1.14  
    1.15  (*Lift and instantiate a rule wrt the given state and subgoal number *)
    1.16  fun lift_inst_rule' (st, i, sinsts, rule) =
    1.17 @@ -340,7 +340,7 @@
    1.18  fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule);
    1.19  
    1.20  (*instantiate variables in the whole state*)
    1.21 -val instantiate_tac = PRIMITIVE o read_instantiate;
    1.22 +val instantiate_tac = PRIMITIVE o Drule.read_instantiate;
    1.23  
    1.24  val instantiate_tac' = PRIMITIVE o Drule.read_instantiate';
    1.25