src/Pure/tactic.ML
changeset 15797 a63605582573
parent 15696 1da4ce092c0b
child 15874 6236cc88d4b8
     1.1 --- a/src/Pure/tactic.ML	Thu Apr 21 19:02:54 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Thu Apr 21 19:12:03 2005 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4    val subgoals_tac      : string list -> int -> tactic
     1.5    val subgoals_of_brl   : bool * thm -> int
     1.6    val term_lift_inst_rule       :
     1.7 -      thm * int * (indexname*typ)list * ((indexname*typ)*term)list  * thm
     1.8 +      thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm
     1.9        -> thm
    1.10    val instantiate_tac   : (string * string) list -> tactic
    1.11    val thin_tac          : string -> int -> tactic
    1.12 @@ -117,6 +117,7 @@
    1.13    val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
    1.14    val eres_inst_tac'    : (indexname * string) list -> thm -> int -> tactic
    1.15    val res_inst_tac'     : (indexname * string) list -> thm -> int -> tactic
    1.16 +  val instantiate_tac'  : (indexname * string) list -> tactic
    1.17  end;
    1.18  
    1.19  structure Tactic: TACTIC =
    1.20 @@ -246,9 +247,7 @@
    1.21                                      Logic.incr_indexes(paramTs,inc) t)
    1.22      (*Lifts instantiation pair over params*)
    1.23      fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
    1.24 -    fun lifttvar((a,i),ctyp) =
    1.25 -        let val {T,sign} = rep_ctyp ctyp
    1.26 -        in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
    1.27 +    val lifttvar = pairself (ctyp_fun (incr_tvar inc))
    1.28  in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
    1.29                       (lift_rule (st,i) rule)
    1.30  end;
    1.31 @@ -278,7 +277,9 @@
    1.32      fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T)
    1.33      (*lift only Var, not term, which must be lifted already*)
    1.34      fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t)
    1.35 -    fun liftTpair((a,i),T) = ((a,i+inc), ctyp_of sign (incr_tvar inc T))
    1.36 +    fun liftTpair (((a, i), S), T) =
    1.37 +      (ctyp_of sign (TVar ((a, i + inc), S)),
    1.38 +       ctyp_of sign (incr_tvar inc T))
    1.39  in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
    1.40                       (lift_rule (st,i) rule)
    1.41  end;
    1.42 @@ -344,6 +345,8 @@
    1.43  (*instantiate variables in the whole state*)
    1.44  val instantiate_tac = PRIMITIVE o read_instantiate;
    1.45  
    1.46 +val instantiate_tac' = PRIMITIVE o Drule.read_instantiate';
    1.47 +
    1.48  (*Deletion of an assumption*)
    1.49  fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
    1.50  
    1.51 @@ -647,7 +650,7 @@
    1.52      val statement = Logic.list_implies (asms, prop);
    1.53      val frees = map Term.dest_Free (Term.term_frees statement);
    1.54      val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
    1.55 -    val fixed_tfrees = foldr Term.add_typ_tfree_names [] (map #2 fixed_frees);
    1.56 +    val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees);
    1.57      val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs;
    1.58  
    1.59      fun err msg = raise ERROR_MESSAGE