src/Pure/Isar/method.ML
changeset 20117 0f7b7bfae82b
parent 20030 e62913ef9d24
child 20224 9c40a144ee0e
     1.1 --- a/src/Pure/Isar/method.ML	Wed Jul 12 21:19:22 2006 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Jul 12 21:19:24 2006 +0200
     1.3 @@ -337,7 +337,7 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -(* rule_tac etc. -- refer to dynamic goal state!! *)
     1.8 +(* rule_tac etc. -- refer to dynamic goal state!! *)   (* FIXME cleanup!! *)
     1.9  
    1.10  fun bires_inst_tac bires_flag ctxt insts thm =
    1.11    let
    1.12 @@ -420,9 +420,7 @@
    1.13        end
    1.14             handle TERM (msg,_)   => (warning msg; no_tac st)
    1.15                  | THM  (msg,_,_) => (warning msg; no_tac st);
    1.16 -  in
    1.17 -    tac
    1.18 -  end;
    1.19 +  in tac end;
    1.20  
    1.21  local
    1.22  
    1.23 @@ -433,19 +431,6 @@
    1.24          quant (insert_tac facts THEN' inst_tac ctxt insts thm))
    1.25    | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
    1.26  
    1.27 -(* Preserve Var indexes of rl; increment revcut_rl instead.
    1.28 -   Copied from tactic.ML *)
    1.29 -fun make_elim_preserve rl =
    1.30 -  let val {maxidx,...} = rep_thm rl
    1.31 -      fun cvar xi = cterm_of ProtoPure.thy (Var(xi,propT));
    1.32 -      val revcut_rl' =
    1.33 -          instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
    1.34 -                             (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
    1.35 -      val arg = (false, rl, nprems_of rl)
    1.36 -      val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
    1.37 -  in  th  end
    1.38 -  handle Bind => raise THM("make_elim_preserve", 1, [rl]);
    1.39 -
    1.40  in
    1.41  
    1.42  val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac;
    1.43 @@ -454,18 +439,18 @@
    1.44  
    1.45  val cut_inst_meth =
    1.46    gen_inst
    1.47 -    (fn ctxt => fn insts => bires_inst_tac false ctxt insts o make_elim_preserve)
    1.48 +    (fn ctxt => fn insts => bires_inst_tac false ctxt insts o Tactic.make_elim_preserve)
    1.49      Tactic.cut_rules_tac;
    1.50  
    1.51  val dres_inst_meth =
    1.52    gen_inst
    1.53 -    (fn ctxt => fn insts => bires_inst_tac true ctxt insts o make_elim_preserve)
    1.54 +    (fn ctxt => fn insts => bires_inst_tac true ctxt insts o Tactic.make_elim_preserve)
    1.55      Tactic.dresolve_tac;
    1.56  
    1.57  val forw_inst_meth =
    1.58    gen_inst
    1.59      (fn ctxt => fn insts => fn rule =>
    1.60 -       bires_inst_tac false ctxt insts (make_elim_preserve rule) THEN'
    1.61 +       bires_inst_tac false ctxt insts (Tactic.make_elim_preserve rule) THEN'
    1.62         assume_tac)
    1.63      Tactic.forward_tac;
    1.64