src/Provers/classical.ML
changeset 52732 b4da1f2ec73f
parent 52699 abed4121c17e
child 54742 7a86358a3c0b
     1.1 --- a/src/Provers/classical.ML	Thu Jul 25 16:46:53 2013 +0200
     1.2 +++ b/src/Provers/classical.ML	Sat Jul 27 16:35:51 2013 +0200
     1.3 @@ -158,7 +158,7 @@
     1.4        val rule'' =
     1.5          rule' |> ALLGOALS (SUBGOAL (fn (goal, i) =>
     1.6            if i = 1 orelse redundant_hyp goal
     1.7 -          then Tactic.etac thin_rl i
     1.8 +          then etac thin_rl i
     1.9            else all_tac))
    1.10          |> Seq.hd
    1.11          |> Drule.zero_var_indexes;
    1.12 @@ -897,9 +897,9 @@
    1.13      val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
    1.14      val rules = rules1 @ rules2 @ rules3 @ rules4;
    1.15      val ruleq = Drule.multi_resolves facts rules;
    1.16 +    val _ = Method.trace ctxt rules;
    1.17    in
    1.18 -    Method.trace ctxt rules;
    1.19 -    fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq
    1.20 +    fn st => Seq.maps (fn rule => rtac rule i st) ruleq
    1.21    end)
    1.22    THEN_ALL_NEW Goal.norm_hhf_tac;
    1.23