# HG changeset patch
# User wenzelm
# Date 1237129183 -3600
# Node ID 92af4e8c54a6141e77b69331d215cec93cb45d38
# Parent  4007ea1ddac28dcf409618da131fd79443cf4670
ML_Syntax.make_binding;

diff -r 4007ea1ddac2 -r 92af4e8c54a6 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Mar 15 15:59:42 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Mar 15 15:59:43 2009 +0100
@@ -155,9 +155,7 @@
     val body = SymbolPos.content (SymbolPos.explode (body_txt, body_pos));
     val txt =
       "local\n\
-      \  val name = " ^ ML_Syntax.print_string name ^ ";\n\
-      \  val pos = " ^ ML_Syntax.print_position pos ^ ";\n\
-      \  val binding = Binding.make (name, pos);\n\
+      \  val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
       \  val body = " ^ body ^ ";\n\
       \in\n\
       \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
diff -r 4007ea1ddac2 -r 92af4e8c54a6 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Sun Mar 15 15:59:42 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Sun Mar 15 15:59:43 2009 +0100
@@ -59,9 +59,8 @@
 
 structure P = OuterParse;
 
-val _ = inline "binding" (Scan.lift (P.position Args.name) >> (fn b =>
-  ML_Syntax.atomic ("Binding.make " ^
-    ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position b)));
+val _ = inline "binding"
+  (Scan.lift (P.position Args.name) >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
 
 val _ = value "theory"
   (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)