# HG changeset patch
# User wenzelm
# Date 1408607339 -7200
# Node ID ff55b42303bc1f2666c656f10bddad04d63a9b45
# Parent  8179d1369567309685ddcbffba7fc7db7eeb5749
tuned;

diff -r 8179d1369567 -r ff55b42303bc src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Aug 20 20:50:28 2014 +0200
+++ b/src/Pure/Isar/method.ML	Thu Aug 21 09:48:59 2014 +0200
@@ -280,7 +280,7 @@
       let
         val context' = context |>
           ML_Context.expression (#pos source)
-            "fun tactic (morphism: morphism) (facts: thm list) : tactic"
+            "fun tactic (morphism: Morphism.morphism) (facts: thm list) : tactic"
             "Method.set_tactic tactic" (ML_Lex.read_source false source);
         val tac = the_tactic context';
       in