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