changeset 30510 | 4120fc59dd85 |
parent 30419 | c944e299eaf9 |
child 30557 | a28d83e903ce |
--- a/src/Pure/Isar/proof.ML Fri Mar 13 19:53:09 2009 +0100 +++ b/src/Pure/Isar/proof.ML Fri Mar 13 19:58:26 2009 +0100 @@ -780,7 +780,7 @@ in (rev vars, props') end; fun refine_terms n = - refine (Method.Basic (K (Method.RAW_METHOD + refine (Method.Basic (K (RAW_METHOD (K (HEADGOAL (PRECISE_CONJUNCTS n (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))), Position.none)) #> Seq.hd;