--- a/src/Pure/Isar/method.ML Wed Nov 30 22:52:46 2005 +0100
+++ b/src/Pure/Isar/method.ML Wed Nov 30 22:52:49 2005 +0100
@@ -211,11 +211,8 @@
(* fact -- composition by facts from context *)
-fun fact_tac [] ctxt [] = ProofContext.some_fact_tac ctxt
- | fact_tac ths _ [] = ProofContext.fact_tac ths
- | fact_tac _ _ facts = EVERY' (map (ProofContext.fact_tac o single) facts);
-
-fun fact rules ctxt = METHOD (fn facts => HEADGOAL (fact_tac rules ctxt facts));
+fun fact [] ctxt = SIMPLE_METHOD' HEADGOAL (ProofContext.some_fact_tac ctxt)
+ | fact rules _ = SIMPLE_METHOD' HEADGOAL (ProofContext.fact_tac rules);
(* assumption *)