eliminated obsolete thm position tags;
authorwenzelm
Sun Nov 15 19:45:05 2009 +0100 (2009-11-15)
changeset 33700768d14a67256
parent 33699 f33b036ef318
child 33701 9dd1079cec3a
eliminated obsolete thm position tags;
src/Pure/Isar/proof_context.ML
src/Pure/Isar/theory_target.ML
src/Pure/ML/ml_thms.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sun Nov 15 19:44:29 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Nov 15 19:45:05 2009 +0100
     1.3 @@ -883,8 +883,7 @@
     1.4            |> singleton (Variable.polymorphic ctxt);
     1.5  
     1.6          fun prove_fact th =
     1.7 -          Goal.prove ctxt [] [] prop (K (ALLGOALS (fact_tac [th])))
     1.8 -          |> Thm.default_position_of th;
     1.9 +          Goal.prove ctxt [] [] prop (K (ALLGOALS (fact_tac [th])));
    1.10          val res =
    1.11            (case get_first (try prove_fact) (potential_facts ctxt prop) of
    1.12              SOME res => res
    1.13 @@ -934,12 +933,12 @@
    1.14      val name = full_name ctxt b;
    1.15      val _ = Context_Position.report_visible ctxt (Markup.local_fact_decl name) pos;
    1.16  
    1.17 -    val facts = PureThy.name_thmss false pos name raw_facts;
    1.18 +    val facts = PureThy.name_thmss false name raw_facts;
    1.19      fun app (th, attrs) x =
    1.20        swap (Library.foldl_map
    1.21          (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th));
    1.22      val (res, ctxt') = fold_map app facts ctxt;
    1.23 -    val thms = PureThy.name_thms false false pos name (flat res);
    1.24 +    val thms = PureThy.name_thms false false name (flat res);
    1.25      val Mode {stmt, ...} = get_mode ctxt;
    1.26    in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
    1.27  
     2.1 --- a/src/Pure/Isar/theory_target.ML	Sun Nov 15 19:44:29 2009 +0100
     2.2 +++ b/src/Pure/Isar/theory_target.ML	Sun Nov 15 19:45:05 2009 +0100
     2.3 @@ -132,7 +132,7 @@
     2.4        |> Drule.zero_var_indexes_list;
     2.5  
     2.6      (*thm definition*)
     2.7 -    val result = PureThy.name_thm true true Position.none name th'';
     2.8 +    val result = PureThy.name_thm true true name th'';
     2.9  
    2.10      (*import fixes*)
    2.11      val (tvars, vars) =
    2.12 @@ -152,7 +152,7 @@
    2.13          NONE => raise THM ("Failed to re-import result", 0, [result'])
    2.14        | SOME res => LocalDefs.trans_props ctxt [res, Thm.symmetric concl_conv])
    2.15        |> Goal.norm_result
    2.16 -      |> PureThy.name_thm false false Position.none name;
    2.17 +      |> PureThy.name_thm false false name;
    2.18  
    2.19    in (result'', result) end;
    2.20  
     3.1 --- a/src/Pure/ML/ml_thms.ML	Sun Nov 15 19:44:29 2009 +0100
     3.2 +++ b/src/Pure/ML/ml_thms.ML	Sun Nov 15 19:45:05 2009 +0100
     3.3 @@ -53,15 +53,14 @@
     3.4  val goal = Scan.unless (by || and_) Args.name;
     3.5  
     3.6  val _ = ML_Context.add_antiq "lemma"
     3.7 -  (fn pos => Args.context -- Args.mode "open" --
     3.8 +  (fn _ => Args.context -- Args.mode "open" --
     3.9        Scan.lift (OuterParse.and_list1 (Scan.repeat1 goal) --
    3.10          (by |-- Method.parse -- Scan.option Method.parse)) >>
    3.11      (fn ((ctxt, is_open), (raw_propss, methods)) => fn {struct_name, background} =>
    3.12        let
    3.13          val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
    3.14          val i = serial ();
    3.15 -        val prep_result =
    3.16 -          Goal.norm_result #> Thm.default_position pos #> not is_open ? Thm.close_derivation;
    3.17 +        val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
    3.18          fun after_qed res goal_ctxt =
    3.19            put_thms (i, map prep_result (ProofContext.export goal_ctxt ctxt (flat res))) goal_ctxt;
    3.20          val ctxt' = ctxt
     4.1 --- a/src/Pure/pure_thy.ML	Sun Nov 15 19:44:29 2009 +0100
     4.2 +++ b/src/Pure/pure_thy.ML	Sun Nov 15 19:45:05 2009 +0100
     4.3 @@ -20,9 +20,9 @@
     4.4    val burrow_facts: ('a list -> 'b list) ->
     4.5      ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
     4.6    val name_multi: string -> 'a list -> (string * 'a) list
     4.7 -  val name_thm: bool -> bool -> Position.T -> string -> thm -> thm
     4.8 -  val name_thms: bool -> bool -> Position.T -> string -> thm list -> thm list
     4.9 -  val name_thmss: bool -> Position.T -> string -> (thm list * 'a) list -> (thm list * 'a) list
    4.10 +  val name_thm: bool -> bool -> string -> thm -> thm
    4.11 +  val name_thms: bool -> bool -> string -> thm list -> thm list
    4.12 +  val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
    4.13    val store_thms: binding * thm list -> theory -> thm list * theory
    4.14    val store_thm: binding * thm -> theory -> thm * theory
    4.15    val store_thm_open: binding * thm -> theory -> thm * theory
    4.16 @@ -122,17 +122,15 @@
    4.17    | name_multi "" xs = map (pair "") xs
    4.18    | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
    4.19  
    4.20 -fun name_thm pre official pos name thm = thm
    4.21 +fun name_thm pre official name thm = thm
    4.22    |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)
    4.23 -  |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name)
    4.24 -  |> Thm.default_position pos
    4.25 -  |> Thm.default_position (Position.thread_data ());
    4.26 +  |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name);
    4.27  
    4.28 -fun name_thms pre official pos name xs =
    4.29 -  map (uncurry (name_thm pre official pos)) (name_multi name xs);
    4.30 +fun name_thms pre official name xs =
    4.31 +  map (uncurry (name_thm pre official)) (name_multi name xs);
    4.32  
    4.33 -fun name_thmss official pos name fact =
    4.34 -  burrow_fact (name_thms true official pos name) fact;
    4.35 +fun name_thmss official name fact =
    4.36 +  burrow_fact (name_thms true official name) fact;
    4.37  
    4.38  
    4.39  (* enter_thms *)
    4.40 @@ -153,20 +151,19 @@
    4.41  
    4.42  (* store_thm(s) *)
    4.43  
    4.44 -fun store_thms (b, thms) = enter_thms (name_thms true true Position.none)
    4.45 -  (name_thms false true Position.none) I (b, thms);
    4.46 +fun store_thms (b, thms) =
    4.47 +  enter_thms (name_thms true true) (name_thms false true) I (b, thms);
    4.48  
    4.49  fun store_thm (b, th) = store_thms (b, [th]) #>> the_single;
    4.50  
    4.51  fun store_thm_open (b, th) =
    4.52 -  enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I
    4.53 -    (b, [th]) #>> the_single;
    4.54 +  enter_thms (name_thms true false) (name_thms false false) I (b, [th]) #>> the_single;
    4.55  
    4.56  
    4.57  (* add_thms(s) *)
    4.58  
    4.59  fun add_thms_atts pre_name ((b, thms), atts) =
    4.60 -  enter_thms pre_name (name_thms false true Position.none)
    4.61 +  enter_thms pre_name (name_thms false true)
    4.62      (Library.foldl_map (Thm.theory_attributes atts)) (b, thms);
    4.63  
    4.64  fun gen_add_thmss pre_name =
    4.65 @@ -175,8 +172,8 @@
    4.66  fun gen_add_thms pre_name args =
    4.67    apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
    4.68  
    4.69 -val add_thmss = gen_add_thmss (name_thms true true Position.none);
    4.70 -val add_thms = gen_add_thms (name_thms true true Position.none);
    4.71 +val add_thmss = gen_add_thmss (name_thms true true);
    4.72 +val add_thms = gen_add_thms (name_thms true true);
    4.73  val add_thm = yield_singleton add_thms;
    4.74  
    4.75  
    4.76 @@ -197,7 +194,7 @@
    4.77  
    4.78      fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
    4.79      val (thms, thy') = thy |> enter_thms
    4.80 -      (name_thmss true pos) (name_thms false true pos) (apsnd flat o Library.foldl_map app)
    4.81 +      (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app)
    4.82        (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts);
    4.83    in ((name, thms), thy') end);
    4.84