| changeset 11718 | 92706a69dacc |
| parent 10464 | b7b916a82dca |
| child 11816 | 545aab7410ac |
--- a/src/Pure/Isar/local_defs.ML Wed Oct 10 18:39:38 2001 +0200 +++ b/src/Pure/Isar/local_defs.ML Wed Oct 10 18:40:46 2001 +0200 @@ -22,7 +22,7 @@ local -val refl_tac = Tactic.rtac (Drule.standard (Drule.reflexive_thm RS Drule.triv_goal)); +val refl_tac = Tactic.rtac (Drule.reflexive_thm RS Drule.triv_goal); fun dest_lhs cprop = let val x = #1 (Logic.dest_equals (Logic.dest_goal (Thm.term_of cprop)))