src/Pure/Isar/theory_target.ML
changeset 24959 119793c84647
parent 24949 5f00e3532418
child 24983 f2f4ba67cef1
     1.1 --- a/src/Pure/Isar/theory_target.ML	Thu Oct 11 15:59:31 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Oct 11 16:05:23 2007 +0200
     1.3 @@ -195,10 +195,10 @@
     1.4      fun const ((c, T), mx) thy =
     1.5        let
     1.6          val U = map #2 xs ---> T;
     1.7 -        val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
     1.8          val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx;
     1.9          val mx3 = if is_loc then NoSyn else mx1;
    1.10 -        val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx3)] thy;
    1.11 +        val (const, thy') = Sign.declare_const (ContextPosition.properties_of lthy) (c, U, mx3) thy;
    1.12 +        val t = Term.list_comb (const, map Free xs);
    1.13        in (((c, mx2), t), thy') end;
    1.14      fun const_class (SOME class) ((c, _), mx) (_, t) =
    1.15            LocalTheory.raw_theory_result (Class.add_const_in_class class ((c, t), mx))
    1.16 @@ -227,7 +227,7 @@
    1.17    in
    1.18      lthy'
    1.19      |> fold2 (const_class some_class) decls abbrs
    1.20 -    |> is_loc ? fold (internal_abbrev loc Syntax.default_mode) abbrs
    1.21 +    |> is_loc ? fold (internal_abbrev loc Syntax.mode_default) abbrs
    1.22      |> LocalTheory.raw_theory (hide_abbrev some_class abbrs)
    1.23          (*FIXME abbreviations should never occur*)
    1.24      |> LocalDefs.add_defs defs