# HG changeset patch
# User haftmann
# Date 1227204363 -3600
# Node ID d6fe93e3dcb93a1e75fd0f8b028b232193770bf2
# Parent  32e83a854e5ee50e2bebf7265575bf1128e959a7
fact table now using name bindings

diff -r 32e83a854e5e -r d6fe93e3dcb9 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Nov 20 19:06:02 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Nov 20 19:06:03 2008 +0100
@@ -23,8 +23,6 @@
   val abbrev_mode: Proof.context -> bool
   val set_stmt: bool -> Proof.context -> Proof.context
   val naming_of: Proof.context -> NameSpace.naming
-  val name_decl: (string * 'a -> Proof.context -> 'b * Proof.context)
-    -> Name.binding * 'a -> Proof.context -> (string * 'b) * Proof.context
   val full_name: Proof.context -> bstring -> string
   val full_binding: Proof.context -> Name.binding -> string
   val consts_of: Proof.context -> Consts.T
@@ -249,18 +247,6 @@
 
 val naming_of = #naming o rep_context;
 
-fun name_decl decl (b, x) ctxt =
-  let
-    val naming = naming_of ctxt;
-    val (naming', name) = Name.namify naming b;
-  in
-    ctxt
-    |> map_naming (K naming')
-    |> decl (Name.name_of b, x)
-    |>> pair name
-    ||> map_naming (K naming)
-  end;
-
 val full_name = NameSpace.full o naming_of;
 val full_binding = NameSpace.full_binding o naming_of;
 
@@ -981,7 +967,7 @@
 
 fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_binding ctxt b))
   | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
-      (Facts.add_local do_props (naming_of ctxt) (full_binding ctxt b, ths));
+      (Facts.add_local do_props (naming_of ctxt) (b, ths) #> snd);
 
 fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
   let
diff -r 32e83a854e5e -r d6fe93e3dcb9 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Thu Nov 20 19:06:02 2008 +0100
+++ b/src/Pure/facts.ML	Thu Nov 20 19:06:03 2008 +0100
@@ -31,9 +31,9 @@
   val props: T -> thm list
   val could_unify: T -> term -> thm list
   val merge: T * T -> T
-  val add_global: NameSpace.naming -> string * thm list -> T -> T
-  val add_local: bool -> NameSpace.naming -> string * thm list -> T -> T
-  val add_dynamic: NameSpace.naming -> string * (Context.generic -> thm list) -> T -> T
+  val add_global: NameSpace.naming -> Name.binding * thm list -> T -> string * T
+  val add_local: bool -> NameSpace.naming -> Name.binding * thm list -> T -> string * T
+  val add_dynamic: NameSpace.naming -> Name.binding * (Context.generic -> thm list) -> T -> string * T
   val del: string -> T -> T
   val hide: bool -> string -> T -> T
 end;
@@ -190,22 +190,20 @@
 
 (* add static entries *)
 
-fun add permissive do_props naming (name, ths) (Facts {facts, props}) =
+fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
   let
-    val facts' =
-      if name = "" then facts
-      else
-        let
-          val (space, tab) = facts;
-          val space' = NameSpace.declare naming name space;
-          val entry = (name, (Static ths, serial ()));
-          val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
-            handle Symtab.DUP dup => err_dup_fact dup;
-        in (space', tab') end;
+    val (name, facts') = if Name.is_nothing b then ("", facts)
+      else let
+        val (space, tab) = facts;
+        val (name, space') = NameSpace.declare_binding naming b space;
+        val entry = (name, (Static ths, serial ()));
+        val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
+          handle Symtab.DUP dup => err_dup_fact dup;
+      in (name, (space', tab')) end;
     val props' =
       if do_props then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
       else props;
-  in make_facts facts' props' end;
+  in (name, make_facts facts' props') end;
 
 val add_global = add false false;
 val add_local = add true;
@@ -213,13 +211,13 @@
 
 (* add dynamic entries *)
 
-fun add_dynamic naming (name, f) (Facts {facts = (space, tab), props}) =
+fun add_dynamic naming (b, f) (Facts {facts = (space, tab), props}) =
   let
-    val space' = NameSpace.declare naming name space;
+    val (name, space') = NameSpace.declare_binding naming b space;
     val entry = (name, (Dynamic f, serial ()));
     val tab' = Symtab.update_new entry tab
       handle Symtab.DUP dup => err_dup_fact dup;
-  in make_facts (space', tab') props end;
+  in (name, make_facts (space', tab') props) end;
 
 
 (* remove entries *)
diff -r 32e83a854e5e -r d6fe93e3dcb9 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Nov 20 19:06:02 2008 +0100
+++ b/src/Pure/pure_thy.ML	Thu Nov 20 19:06:03 2008 +0100
@@ -152,7 +152,7 @@
     val (thy', thms') =
       enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
     val thms'' = map (Thm.transfer thy') thms';
-    val thy'' = thy' |> FactsData.map (apfst (Facts.add_global naming (name, thms'')));
+    val thy'' = thy' |> (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
   in (thms'', thy'') end;
 
 
@@ -187,9 +187,9 @@
 
 (* add_thms_dynamic *)
 
-fun add_thms_dynamic (bname, f) thy =
-  let val name = Sign.full_name thy bname
-  in thy |> FactsData.map (apfst (Facts.add_dynamic (Sign.naming_of thy) (name, f))) end;
+fun add_thms_dynamic (bname, f) thy = thy
+  |> (FactsData.map o apfst)
+      (Facts.add_dynamic (Sign.naming_of thy) (Name.binding bname, f) #> snd);
 
 
 (* note_thmss *)