src/Pure/Isar/theory_target.ML
changeset 24949 5f00e3532418
parent 24939 6dd60d1191bf
child 24959 119793c84647
     1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Oct 10 17:31:55 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Oct 10 17:31:56 2007 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4        (Sign.add_abbrev Syntax.internalM [] arg') (ProofContext.add_abbrev Syntax.internalM [] arg')
     1.5      #-> (fn (lhs, _) =>
     1.6        Term.equiv_types (rhs, rhs') ?
     1.7 -        Morphism.form (ProofContext.target_notation prmode [(lhs, mx)])))
     1.8 +        Morphism.form (ProofContext.target_notation true prmode [(lhs, mx)])))
     1.9    end;
    1.10  
    1.11  fun internal_abbrev loc prmode ((c, mx), t) lthy = lthy
    1.12 @@ -279,10 +279,11 @@
    1.13      lthy
    1.14      |> LocalTheory.theory_result
    1.15          (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u'))
    1.16 -    |-> (fn (lhs as Const (full_c, _), rhs) => LocalTheory.theory (Sign.add_notation prmode [(lhs, mx3)])
    1.17 -    #> is_loc ? internal_abbrev loc prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs))
    1.18 -    #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1)
    1.19 -    #> local_abbrev (c, rhs))
    1.20 +    |-> (fn (lhs as Const (full_c, _), rhs) =>
    1.21 +          LocalTheory.theory (Sign.notation true prmode [(lhs, mx3)])
    1.22 +          #> is_loc ? internal_abbrev loc prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs))
    1.23 +          #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1)
    1.24 +          #> local_abbrev (c, rhs))
    1.25    end;
    1.26  
    1.27