--- a/src/Pure/Isar/method.ML Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/Isar/method.ML Thu Apr 27 15:06:35 2006 +0200
@@ -265,7 +265,7 @@
let
val rules =
if not (null arg_rules) then arg_rules
- else List.concat (ContextRules.find_rules false facts goal ctxt)
+ else flat (ContextRules.find_rules false facts goal ctxt)
in trace ctxt rules; tac rules facts i end);
fun meth tac x = METHOD (HEADGOAL o tac x);
@@ -617,7 +617,7 @@
local
fun sect ss = Scan.first (map Scan.lift ss);
-fun thms ss = Scan.repeat (Scan.unless (sect ss) Attrib.multi_thm) >> List.concat;
+fun thms ss = Scan.repeat (Scan.unless (sect ss) Attrib.multi_thm) >> flat;
fun app (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths);