# HG changeset patch
# User wenzelm
# Date 1258310705 -3600
# Node ID 768d14a67256a901df3657b7f9075bb8ea68acac
# Parent  f33b036ef3183a7462ee5c0080e088d3ecee4b47
eliminated obsolete thm position tags;

diff -r f33b036ef318 -r 768d14a67256 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Nov 15 19:44:29 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Nov 15 19:45:05 2009 +0100
@@ -883,8 +883,7 @@
           |> singleton (Variable.polymorphic ctxt);
 
         fun prove_fact th =
-          Goal.prove ctxt [] [] prop (K (ALLGOALS (fact_tac [th])))
-          |> Thm.default_position_of th;
+          Goal.prove ctxt [] [] prop (K (ALLGOALS (fact_tac [th])));
         val res =
           (case get_first (try prove_fact) (potential_facts ctxt prop) of
             SOME res => res
@@ -934,12 +933,12 @@
     val name = full_name ctxt b;
     val _ = Context_Position.report_visible ctxt (Markup.local_fact_decl name) pos;
 
-    val facts = PureThy.name_thmss false pos name raw_facts;
+    val facts = PureThy.name_thmss false name raw_facts;
     fun app (th, attrs) x =
       swap (Library.foldl_map
         (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th));
     val (res, ctxt') = fold_map app facts ctxt;
-    val thms = PureThy.name_thms false false pos name (flat res);
+    val thms = PureThy.name_thms false false name (flat res);
     val Mode {stmt, ...} = get_mode ctxt;
   in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
 
diff -r f33b036ef318 -r 768d14a67256 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sun Nov 15 19:44:29 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sun Nov 15 19:45:05 2009 +0100
@@ -132,7 +132,7 @@
       |> Drule.zero_var_indexes_list;
 
     (*thm definition*)
-    val result = PureThy.name_thm true true Position.none name th'';
+    val result = PureThy.name_thm true true name th'';
 
     (*import fixes*)
     val (tvars, vars) =
@@ -152,7 +152,7 @@
         NONE => raise THM ("Failed to re-import result", 0, [result'])
       | SOME res => LocalDefs.trans_props ctxt [res, Thm.symmetric concl_conv])
       |> Goal.norm_result
-      |> PureThy.name_thm false false Position.none name;
+      |> PureThy.name_thm false false name;
 
   in (result'', result) end;
 
diff -r f33b036ef318 -r 768d14a67256 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Sun Nov 15 19:44:29 2009 +0100
+++ b/src/Pure/ML/ml_thms.ML	Sun Nov 15 19:45:05 2009 +0100
@@ -53,15 +53,14 @@
 val goal = Scan.unless (by || and_) Args.name;
 
 val _ = ML_Context.add_antiq "lemma"
-  (fn pos => Args.context -- Args.mode "open" --
+  (fn _ => Args.context -- Args.mode "open" --
       Scan.lift (OuterParse.and_list1 (Scan.repeat1 goal) --
         (by |-- Method.parse -- Scan.option Method.parse)) >>
     (fn ((ctxt, is_open), (raw_propss, methods)) => fn {struct_name, background} =>
       let
         val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
         val i = serial ();
-        val prep_result =
-          Goal.norm_result #> Thm.default_position pos #> not is_open ? Thm.close_derivation;
+        val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
         fun after_qed res goal_ctxt =
           put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt (flat res))) goal_ctxt;
         val ctxt' = ctxt
diff -r f33b036ef318 -r 768d14a67256 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);