changeset 18473 | 8bf56053475a |
parent 18450 | e57731ba01dd |
child 18502 | 24efc1587f9d |
--- a/src/Pure/Isar/locale.ML Thu Dec 22 00:29:03 2005 +0100 +++ b/src/Pure/Isar/locale.ML Thu Dec 22 00:29:04 2005 +0100 @@ -2110,7 +2110,7 @@ val refine_protected = Proof.refine (Method.Basic (K (Method.RAW_METHOD - (K (ALLGOALS (CONJUNCTS (ALLGOALS (Tactic.rtac Drule.protectI)))))))) + (K (ALLGOALS (CONJUNCTS2 ~1 (ALLGOALS (Tactic.rtac Drule.protectI)))))))) #> Seq.hd; fun goal_name thy kind target propss =