# HG changeset patch
# User wenzelm
# Date 1133387569 -3600
# Node ID 5ca7ba291f35b1b41f852be623780c8789641f68
# Parent  f18a54840629e63901df2551a5fb746cf1a7bded
method 'fact': SIMPLE_METHOD, i.e. insert facts;

diff -r f18a54840629 -r 5ca7ba291f35 src/Pure/Isar/method.ML
--- 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 *)