tuned abbrev interface;
authorwenzelm
Sat Oct 20 18:54:34 2007 +0200 (2007-10-20)
changeset 25121fbea3ca04d51
parent 25120 23fbc38f6432
child 25122 f37d7dd25c88
tuned abbrev interface;
PrintMode.internal;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Sat Oct 20 18:54:33 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Oct 20 18:54:34 2007 +0200
     1.3 @@ -177,8 +177,8 @@
     1.4      val arg = (c', Term.close_schematic_term rhs');
     1.5    in
     1.6      Context.mapping_result
     1.7 -      (Sign.add_abbrev Syntax.internalM pos legacy_arg)
     1.8 -      (ProofContext.add_abbrev Syntax.internalM pos arg)
     1.9 +      (Sign.add_abbrev PrintMode.internal pos legacy_arg)
    1.10 +      (ProofContext.add_abbrev PrintMode.internal pos arg)
    1.11      #-> (fn (lhs' as Const (d, _), _) =>
    1.12          Type.similar_types (rhs, rhs') ?
    1.13            (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
    1.14 @@ -215,25 +215,22 @@
    1.15      val u = fold_rev lambda xs t';
    1.16      val global_rhs =
    1.17        singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
    1.18 -
    1.19 -    val lthy' =
    1.20 -      if is_locale then
    1.21 -        lthy
    1.22 -        |> LocalTheory.theory_result (Sign.add_abbrev Syntax.internalM pos (c, global_rhs))
    1.23 -        |-> (fn (lhs, _) =>
    1.24 +  in
    1.25 +    lthy |>
    1.26 +     (if is_locale then
    1.27 +        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal pos (c, global_rhs))
    1.28 +        #-> (fn (lhs, _) =>
    1.29            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    1.30              term_syntax ta (locale_const prmode pos ((c, mx2), lhs')) #>
    1.31 -            is_class ? class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), lhs'))
    1.32 +            is_class ?
    1.33 +              class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), lhs'))
    1.34            end)
    1.35        else
    1.36 -        lthy
    1.37 -        |> LocalTheory.theory
    1.38 +        LocalTheory.theory
    1.39            (Sign.add_abbrev (#1 prmode) pos (c, global_rhs) #-> (fn (lhs, _) =>
    1.40 -           Sign.notation true prmode [(lhs, mx3)]))
    1.41 -  in
    1.42 -    lthy'
    1.43 -    |> ProofContext.add_abbrev Syntax.internalM pos (c, t) |> snd
    1.44 -    |> LocalDefs.add_def ((c, NoSyn), t)
    1.45 +           Sign.notation true prmode [(lhs, mx3)])))
    1.46 +    |> ProofContext.add_abbrev PrintMode.internal pos (c, t) |> snd
    1.47 +    |> LocalDefs.fixed_abbrev ((c, NoSyn), t)
    1.48    end;
    1.49  
    1.50