src/Pure/Isar/theory_target.ML
changeset 25096 b8950f7cf92e
parent 25083 765528b4b419
child 25105 c9f67836c4d8
     1.1 --- a/src/Pure/Isar/theory_target.ML	Fri Oct 19 12:22:12 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Oct 19 15:08:33 2007 +0200
     1.3 @@ -195,7 +195,7 @@
     1.4          val t = Term.list_comb (const, map Free xs);
     1.5        in (((c, mx12), t), thy') end;
     1.6      fun class_const ((c, _), _) ((_, (mx1, _)), t) =
     1.7 -      LocalTheory.raw_theory_result (Class.add_logical_const target ((c, mx1), t))
     1.8 +      LocalTheory.raw_theory_result (Class.add_logical_const target pos ((c, mx1), t))
     1.9        #> snd
    1.10        #> LocalTheory.target (Class.refresh_syntax target);
    1.11  
    1.12 @@ -218,9 +218,9 @@
    1.13    |> ProofContext.add_abbrev Syntax.internalM pos (c, t) |> snd
    1.14    |> LocalDefs.add_def ((c, NoSyn), t);
    1.15  
    1.16 -fun class_abbrev target prmode ((c, mx), rhs) lthy = lthy   (* FIXME pos *)
    1.17 -  |> LocalTheory.raw_theory_result (Class.add_syntactic_const target prmode
    1.18 -      ((c, mx), rhs))
    1.19 +fun class_abbrev target prmode pos ((c, mx), rhs) lthy = lthy
    1.20 +  |> LocalTheory.raw_theory_result
    1.21 +       (Class.add_syntactic_const target prmode pos ((c, mx), rhs))
    1.22    |> snd
    1.23    |> LocalTheory.target (Class.refresh_syntax target);
    1.24  
    1.25 @@ -248,7 +248,7 @@
    1.26        |-> (fn (lhs, _) =>
    1.27          let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    1.28            term_syntax ta (locale_const prmode pos ((c, mx2), lhs')) #>
    1.29 -          is_class ? class_abbrev target prmode ((c, mx1), lhs')
    1.30 +          is_class ? class_abbrev target prmode pos ((c, mx1), lhs')
    1.31          end)
    1.32        |> context_abbrev pos (c, raw_t)
    1.33      else