# 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 *)