src/Pure/tactic.ML
changeset 19532 dae447f2b0b4
parent 19482 9f11af8f7ef9
child 19743 0843210d3756
     1.1 --- a/src/Pure/tactic.ML	Tue May 02 00:33:40 2006 +0200
     1.2 +++ b/src/Pure/tactic.ML	Tue May 02 14:27:49 2006 +0200
     1.3 @@ -230,15 +230,12 @@
     1.4    in rename_wrt_term Bi (Logic.strip_params Bi) end;
     1.5  
     1.6  (*params of subgoal i as they are printed*)
     1.7 -fun params_of_state st i =
     1.8 -  let val (_, _, Bi, _) = dest_state(st,i)
     1.9 -      val params = Logic.strip_params Bi
    1.10 -  in rev(rename_wrt_term Bi params) end;
    1.11 +fun params_of_state i st = rev (innermost_params i st);
    1.12  
    1.13  (*read instantiations with respect to subgoal i of proof state st*)
    1.14  fun read_insts_in_state (st, i, sinsts, rule) =
    1.15    let val thy = Thm.theory_of_thm st
    1.16 -      and params = params_of_state st i
    1.17 +      and params = params_of_state i st
    1.18        and rts = types_sorts rule and (types,sorts) = types_sorts st
    1.19        fun types'(a, ~1) = (case AList.lookup (op =) params a of NONE => types (a, ~1) | sm => sm)
    1.20          | types' ixn = types ixn;
    1.21 @@ -249,7 +246,7 @@
    1.22  fun lift_inst_rule' (st, i, sinsts, rule) =
    1.23  let val (Tinsts,insts) = read_insts_in_state (st, i, sinsts, rule)
    1.24      and {maxidx,...} = rep_thm st
    1.25 -    and params = params_of_state st i
    1.26 +    and params = params_of_state i st
    1.27      val paramTs = map #2 params
    1.28      and inc = maxidx+1
    1.29      fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
    1.30 @@ -283,7 +280,7 @@
    1.31  *)
    1.32  fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
    1.33  let val {maxidx,thy,...} = rep_thm st
    1.34 -    val paramTs = map #2 (params_of_state st i)
    1.35 +    val paramTs = map #2 (params_of_state i st)
    1.36      and inc = maxidx+1
    1.37      fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
    1.38      (*lift only Var, not term, which must be lifted already*)