implicit use of LocalTheory.group etc.;
authorwenzelm
Mon Feb 25 16:31:20 2008 +0100 (2008-02-25)
changeset 26132c927c3ed82c9
parent 26131 91024979b9eb
child 26133 8ea867ad9a48
implicit use of LocalTheory.group etc.;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Feb 25 16:31:19 2008 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Feb 25 16:31:20 2008 +0100
     1.3 @@ -151,7 +151,7 @@
     1.4    |> ProofContext.note_thmss_i kind facts
     1.5    ||> ProofContext.restore_naming ctxt;
     1.6  
     1.7 -fun notes (Target {target, is_locale, ...}) kind group facts lthy =
     1.8 +fun notes (Target {target, is_locale, ...}) kind facts lthy =
     1.9    let
    1.10      val thy = ProofContext.theory_of lthy;
    1.11      val full = LocalTheory.full_name lthy;
    1.12 @@ -168,7 +168,7 @@
    1.13    in
    1.14      lthy |> LocalTheory.theory
    1.15        (Sign.qualified_names
    1.16 -        #> PureThy.note_thmss_grouped kind group global_facts #> snd
    1.17 +        #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
    1.18          #> Sign.restore_naming thy)
    1.19  
    1.20      |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
    1.21 @@ -185,7 +185,7 @@
    1.22    else if not is_class then (NoSyn, mx, NoSyn)
    1.23    else (mx, NoSyn, NoSyn);
    1.24  
    1.25 -fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) pos ((c, mx), rhs) phi =
    1.26 +fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi =
    1.27    let
    1.28      val c' = Morphism.name phi c;
    1.29      val rhs' = Morphism.term phi rhs;
    1.30 @@ -197,8 +197,8 @@
    1.31    in
    1.32      not (is_class andalso (similar_body orelse class_global)) ?
    1.33        (Context.mapping_result
    1.34 -        (Sign.add_abbrev PrintMode.internal pos legacy_arg)
    1.35 -        (ProofContext.add_abbrev PrintMode.internal pos arg)
    1.36 +        (Sign.add_abbrev PrintMode.internal tags legacy_arg)
    1.37 +        (ProofContext.add_abbrev PrintMode.internal tags arg)
    1.38        #-> (fn (lhs' as Const (d, _), _) =>
    1.39            similar_body ?
    1.40              (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
    1.41 @@ -207,7 +207,7 @@
    1.42  
    1.43  fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((c, T), mx) lthy =
    1.44    let
    1.45 -    val pos = Position.properties_of (Position.thread_data ());
    1.46 +    val tags = LocalTheory.group_position_of lthy;
    1.47      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.48      val U = map #2 xs ---> T;
    1.49      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.50 @@ -224,13 +224,13 @@
    1.51                  if mx3 <> NoSyn then syntax_error c'
    1.52                  else LocalTheory.theory_result (Overloading.declare (c', U))
    1.53                    ##> Overloading.confirm c
    1.54 -            | NONE => LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3))));
    1.55 +            | NONE => LocalTheory.theory_result (Sign.declare_const tags (c, U, mx3))));
    1.56      val (const, lthy') = lthy |> declare_const;
    1.57      val t = Term.list_comb (const, map Free xs);
    1.58    in
    1.59      lthy'
    1.60 -    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default pos ((c, mx2), t))
    1.61 -    |> is_class ? class_target ta (Class.declare target pos ((c, mx1), t))
    1.62 +    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default tags ((c, mx2), t))
    1.63 +    |> is_class ? class_target ta (Class.declare target tags ((c, mx1), t))
    1.64      |> LocalDefs.add_def ((c, NoSyn), t)
    1.65    end;
    1.66  
    1.67 @@ -239,7 +239,7 @@
    1.68  
    1.69  fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((c, mx), t) lthy =
    1.70    let
    1.71 -    val pos = Position.properties_of (Position.thread_data ());
    1.72 +    val tags = LocalTheory.group_position_of lthy;
    1.73      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    1.74      val target_ctxt = LocalTheory.target_of lthy;
    1.75  
    1.76 @@ -252,17 +252,17 @@
    1.77    in
    1.78      lthy |>
    1.79       (if is_locale then
    1.80 -        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal pos (c, global_rhs))
    1.81 +        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal tags (c, global_rhs))
    1.82          #-> (fn (lhs, _) =>
    1.83            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    1.84 -            term_syntax ta (locale_const ta prmode pos ((c, mx2), lhs')) #>
    1.85 -            is_class ? class_target ta (Class.abbrev target prmode pos ((c, mx1), t'))
    1.86 +            term_syntax ta (locale_const ta prmode tags ((c, mx2), lhs')) #>
    1.87 +            is_class ? class_target ta (Class.abbrev target prmode tags ((c, mx1), t'))
    1.88            end)
    1.89        else
    1.90          LocalTheory.theory
    1.91 -          (Sign.add_abbrev (#1 prmode) pos (c, global_rhs) #-> (fn (lhs, _) =>
    1.92 +          (Sign.add_abbrev (#1 prmode) tags (c, global_rhs) #-> (fn (lhs, _) =>
    1.93             Sign.notation true prmode [(lhs, mx3)])))
    1.94 -    |> ProofContext.add_abbrev PrintMode.internal pos (c, t) |> snd
    1.95 +    |> ProofContext.add_abbrev PrintMode.internal tags (c, t) |> snd
    1.96      |> LocalDefs.fixed_abbrev ((c, NoSyn), t)
    1.97    end;
    1.98  
    1.99 @@ -270,7 +270,7 @@
   1.100  (* define *)
   1.101  
   1.102  fun define (ta as Target {target, is_locale, is_class, ...})
   1.103 -    kind group ((c, mx), ((name, atts), rhs)) lthy =
   1.104 +    kind ((c, mx), ((name, atts), rhs)) lthy =
   1.105    let
   1.106      val thy = ProofContext.theory_of lthy;
   1.107      val thy_ctxt = ProofContext.init thy;
   1.108 @@ -303,13 +303,13 @@
   1.109  
   1.110      (*note*)
   1.111      val ([(res_name, [res])], lthy4) = lthy3
   1.112 -      |> notes ta kind group [((name', atts), [([def], [])])];
   1.113 +      |> notes ta kind [((name', atts), [([def], [])])];
   1.114    in ((lhs, (res_name, res)), lthy4) end;
   1.115  
   1.116  
   1.117  (* axioms *)
   1.118  
   1.119 -fun axioms ta kind group (vars, specs) lthy =
   1.120 +fun axioms ta kind (vars, specs) lthy =
   1.121    let
   1.122      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
   1.123      val expanded_props = map (Assumption.export_term lthy thy_ctxt) (maps snd specs);
   1.124 @@ -329,7 +329,7 @@
   1.125      |> fold Variable.declare_term expanded_props
   1.126      |> LocalTheory.theory (fold (fn c => Theory.add_deps "" c []) global_consts)
   1.127      |> LocalTheory.theory_result (fold_map axiom specs)
   1.128 -    |-> notes ta kind group
   1.129 +    |-> notes ta kind
   1.130      |>> pair (map #1 consts)
   1.131    end;
   1.132