src/Provers/classical.ML
changeset 21963 416a5338d2bb
parent 21689 58abd6d8abd1
child 22095 07875394618e
     1.1 --- a/src/Provers/classical.ML	Sat Dec 30 16:08:00 2006 +0100
     1.2 +++ b/src/Provers/classical.ML	Sat Dec 30 16:08:03 2006 +0100
     1.3 @@ -194,8 +194,7 @@
     1.4            then Tactic.etac thin_rl i
     1.5            else all_tac))
     1.6          |> Seq.hd
     1.7 -        |> Drule.zero_var_indexes
     1.8 -        |> PureThy.put_name_hint (PureThy.get_name_hint rule);
     1.9 +        |> Drule.zero_var_indexes;
    1.10      in if Drule.equiv_thm (rule, rule'') then rule else rule'' end
    1.11    else rule;
    1.12