src/Pure/Isar/isar_cmd.ML
changeset 30288 a32700e45ab3
parent 30242 aea5d7fa7ef5
child 30334 a2f236a717fa
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 05 18:19:20 2009 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Mar 05 19:48:02 2009 +0100
     1.3 @@ -150,10 +150,12 @@
     1.4      val oracle = SymbolPos.content (SymbolPos.explode (oracle_txt, pos));
     1.5      val txt =
     1.6        "local\n\
     1.7 -      \  val name = " ^ quote name ^ ";\n\
     1.8 +      \  val name = " ^ ML_Syntax.print_string name ^ ";\n\
     1.9 +      \  val pos = " ^ ML_Syntax.print_position pos ^ ";\n\
    1.10 +      \  val binding = Binding.make (name, pos);\n\
    1.11        \  val oracle = " ^ oracle ^ ";\n\
    1.12        \in\n\
    1.13 -      \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (name, oracle))));\n\
    1.14 +      \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, oracle))));\n\
    1.15        \end;\n";
    1.16    in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false pos txt)) end;
    1.17