# HG changeset patch
# User wenzelm
# Date 1152200855 -7200
# Node ID f5c39548101e004384c45ad507523ab45ba46c31
# Parent  e62913ef9d2485e22310796b85650f9f64542f69
apply_text: support Method.Source_i;

diff -r e62913ef9d24 -r f5c39548101e 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)