apply_text: support Method.Source_i;
authorwenzelm
Thu, 06 Jul 2006 17:47:35 +0200
changeset 20031 f5c39548101e
parent 20030 e62913ef9d24
child 20032 2087e5634598
apply_text: support Method.Source_i;
src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Jul 06 17:47:34 2006 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Jul 06 17:47:35 2006 +0200
@@ -423,6 +423,7 @@
 
     fun eval (Method.Basic m) = apply_method cc m
       | eval (Method.Source src) = apply_method cc (Method.method thy src)
+      | eval (Method.Source_i src) = apply_method cc (Method.method_i thy src)
       | eval (Method.Then txts) = Seq.EVERY (map eval txts)
       | eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
       | eval (Method.Try txt) = Seq.TRY (eval txt)