src/Pure/Isar/method.ML
changeset 42380 9371ea9f91fb
parent 42375 774df7c59508
child 42616 92715b528e78
     1.1 --- a/src/Pure/Isar/method.ML	Sun Apr 17 21:04:22 2011 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Sun Apr 17 21:17:45 2011 +0200
     1.3 @@ -356,12 +356,12 @@
     1.4  
     1.5  fun method_i thy =
     1.6    let
     1.7 -    val meths = #2 (Methods.get thy);
     1.8 +    val (space, tab) = Methods.get thy;
     1.9      fun meth src =
    1.10        let val ((name, _), pos) = Args.dest_src src in
    1.11 -        (case Symtab.lookup meths name of
    1.12 +        (case Symtab.lookup tab name of
    1.13            NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
    1.14 -        | SOME (mth, _) => (Position.report pos (Markup.method name); mth src))
    1.15 +        | SOME (mth, _) => (Position.report pos (Name_Space.markup space name); mth src))
    1.16        end;
    1.17    in meth end;
    1.18