# HG changeset patch
# User wenzelm
# Date 1236424050 -3600
# Node ID eb189f7e43a1aaee2998270c0dc4851feb42e1e1
# Parent  efd1bec4630a0ee257ef59ce039026ba7fb21a6a
Theory.add_axioms/add_defs: replaced old bstring by binding;

diff -r efd1bec4630a -r eb189f7e43a1 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 07 11:45:56 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 07 12:07:30 2009 +0100
@@ -163,7 +163,7 @@
 (* axioms *)
 
 fun add_axms f args thy =
-  f (map (fn ((b, ax), srcs) => ((Binding.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy;
+  f (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args) thy;
 
 val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
 
diff -r efd1bec4630a -r eb189f7e43a1 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Mar 07 11:45:56 2009 +0100
+++ b/src/Pure/pure_thy.ML	Sat Mar 07 12:07:30 2009 +0100
@@ -36,14 +36,14 @@
   val note_thmss_grouped: string -> string -> (Thm.binding *
       (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
   val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
-  val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
+  val add_axioms_cmd: ((binding * string) * attribute list) list -> theory -> thm list * theory
   val add_defs: bool -> ((binding * term) * attribute list) list ->
     theory -> thm list * theory
   val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
     theory -> thm list * theory
-  val add_defs_cmd: bool -> ((bstring * string) * attribute list) list ->
+  val add_defs_cmd: bool -> ((binding * string) * attribute list) list ->
     theory -> thm list * theory
-  val add_defs_unchecked_cmd: bool -> ((bstring * string) * attribute list) list ->
+  val add_defs_unchecked_cmd: bool -> ((binding * string) * attribute list) list ->
     theory -> thm list * theory
   val old_appl_syntax: theory -> bool
   val old_appl_syntax_setup: theory -> theory
@@ -227,19 +227,19 @@
 local
   fun get_ax thy (b, _) = Thm.axiom thy (Sign.full_name thy b);
   fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs;
-  fun add_axm prep_b add = fold_map (fn ((b, ax), atts) => fn thy =>
+  fun add_axm add = fold_map (fn ((b, ax), atts) => fn thy =>
     let
       val named_ax = [(b, ax)];
       val thy' = add named_ax thy;
-      val thm = hd (get_axs thy' ((map o apfst) prep_b named_ax));
-    in apfst hd (gen_add_thms (K I) [((prep_b b, thm), atts)] thy') end);
+      val thm = hd (get_axs thy' named_ax);
+    in apfst hd (gen_add_thms (K I) [((b, thm), atts)] thy') end);
 in
-  val add_defs               = add_axm I o Theory.add_defs_i false;
-  val add_defs_unchecked     = add_axm I o Theory.add_defs_i true;
-  val add_axioms             = add_axm I Theory.add_axioms_i;
-  val add_defs_cmd           = add_axm Binding.name o Theory.add_defs false;
-  val add_defs_unchecked_cmd = add_axm Binding.name o Theory.add_defs true;
-  val add_axioms_cmd         = add_axm Binding.name Theory.add_axioms;
+  val add_defs               = add_axm o Theory.add_defs_i false;
+  val add_defs_unchecked     = add_axm o Theory.add_defs_i true;
+  val add_axioms             = add_axm Theory.add_axioms_i;
+  val add_defs_cmd           = add_axm o Theory.add_defs false;
+  val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
+  val add_axioms_cmd         = add_axm Theory.add_axioms;
 end;
 
 
@@ -389,6 +389,6 @@
   #> Sign.hide_const false "Pure.sort_constraint"
   #> Sign.hide_const false "Pure.conjunction"
   #> add_thmss [((Binding.name "nothing", []), [])] #> snd
-  #> Theory.add_axioms_i ((map o apfst) Binding.name Proofterm.equality_axms)));
+  #> Theory.add_axioms_i (map (apfst Binding.name) Proofterm.equality_axms)));
 
 end;
diff -r efd1bec4630a -r eb189f7e43a1 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Mar 07 11:45:56 2009 +0100
+++ b/src/Pure/theory.ML	Sat Mar 07 12:07:30 2009 +0100
@@ -29,10 +29,10 @@
   val begin_theory: string -> theory list -> theory
   val end_theory: theory -> theory
   val add_axioms_i: (binding * term) list -> theory -> theory
-  val add_axioms: (bstring * string) list -> theory -> theory
+  val add_axioms: (binding * string) list -> theory -> theory
   val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
   val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
-  val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory
+  val add_defs: bool -> bool -> (binding * string) list -> theory -> theory
   val add_finals_i: bool -> term list -> theory -> theory
   val add_finals: bool -> string list -> theory -> theory
   val specify_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
@@ -153,9 +153,6 @@
 
 (* prepare axioms *)
 
-fun err_in_axm msg name =
-  cat_error msg ("The error(s) above occurred in axiom " ^ quote name);
-
 fun cert_axm thy (b, raw_tm) =
   let
     val (t, T, _) = Sign.certify_prop thy raw_tm
@@ -166,9 +163,9 @@
     (b, Sign.no_vars (Syntax.pp_global thy) t)
   end;
 
-fun read_axm thy (bname, str) =
-  cert_axm thy (Binding.name bname, Syntax.read_prop_global thy str)
-    handle ERROR msg => err_in_axm msg bname;
+fun read_axm thy (b, str) =
+  cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg =>
+    cat_error msg ("The error(s) above occurred in axiom: " ^ quote (Binding.str_of b));
 
 
 (* add_axioms(_i) *)