src/Pure/pure_thy.ML

--- a/src/Pure/pure_thy.ML	Sun Nov 15 19:44:29 2009 +0100
+++ b/src/Pure/pure_thy.ML	Sun Nov 15 19:45:05 2009 +0100
@@ -20,9 +20,9 @@
   val burrow_facts: ('a list -> 'b list) ->
     ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
   val name_multi: string -> 'a list -> (string * 'a) list
-  val name_thm: bool -> bool -> Position.T -> string -> thm -> thm
-  val name_thms: bool -> bool -> Position.T -> string -> thm list -> thm list
-  val name_thmss: bool -> Position.T -> string -> (thm list * 'a) list -> (thm list * 'a) list
+  val name_thm: bool -> bool -> string -> thm -> thm
+  val name_thms: bool -> bool -> string -> thm list -> thm list
+  val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
   val store_thms: binding * thm list -> theory -> thm list * theory
   val store_thm: binding * thm -> theory -> thm * theory
   val store_thm_open: binding * thm -> theory -> thm * theory
@@ -122,17 +122,15 @@
   | name_multi "" xs = map (pair "") xs
   | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
 
-fun name_thm pre official pos name thm = thm
+fun name_thm pre official name thm = thm
   |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)
-  |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name)
-  |> Thm.default_position pos
-  |> Thm.default_position (Position.thread_data ());
+  |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name);
 
-fun name_thms pre official pos name xs =
-  map (uncurry (name_thm pre official pos)) (name_multi name xs);
+fun name_thms pre official name xs =
+  map (uncurry (name_thm pre official)) (name_multi name xs);
 
-fun name_thmss official pos name fact =
-  burrow_fact (name_thms true official pos name) fact;
+fun name_thmss official name fact =
+  burrow_fact (name_thms true official name) fact;
 
 
 (* enter_thms *)
@@ -153,20 +151,19 @@
 
 (* store_thm(s) *)
 
-fun store_thms (b, thms) = enter_thms (name_thms true true Position.none)
-  (name_thms false true Position.none) I (b, thms);
+fun store_thms (b, thms) =
+  enter_thms (name_thms true true) (name_thms false true) I (b, thms);
 
 fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
 
 fun store_thm_open (b, th) =
-  enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I
-    (b, [th]) #>> the_single;
+  enter_thms (name_thms true false) (name_thms false false) I (b, [th]) #>> the_single;
 
 
 (* add_thms(s) *)
 
 fun add_thms_atts pre_name ((b, thms), atts) =
-  enter_thms pre_name (name_thms false true Position.none)
+  enter_thms pre_name (name_thms false true)
     (Library.foldl_map (Thm.theory_attributes atts)) (b, thms);
 
 fun gen_add_thmss pre_name =
@@ -175,8 +172,8 @@
 fun gen_add_thms pre_name args =
   apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
 
-val add_thmss = gen_add_thmss (name_thms true true Position.none);
-val add_thms = gen_add_thms (name_thms true true Position.none);
+val add_thmss = gen_add_thmss (name_thms true true);
+val add_thms = gen_add_thms (name_thms true true);
 val add_thm = yield_singleton add_thms;
 
 
@@ -197,7 +194,7 @@
 
     fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
     val (thms, thy') = thy |> enter_thms
-      (name_thmss true pos) (name_thms false true pos) (apsnd flat o Library.foldl_map app)
+      (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app)
       (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts);
   in ((name, thms), thy') end);