TermSyntax.abbrev;
authorwenzelm
Sat Dec 09 18:05:49 2006 +0100 (2006-12-09)
changeset 217297b3ccdae9212
parent 21728 906649272ba0
child 21730 88d8b4052792
TermSyntax.abbrev;
ProofContext.set_expand_abbrevs;
src/Pure/Isar/specification.ML
     1.1 --- a/src/Pure/Isar/specification.ML	Sat Dec 09 18:05:48 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Sat Dec 09 18:05:49 2006 +0100
     1.3 @@ -146,14 +146,14 @@
     1.4    let
     1.5      val ((vars, [(_, [prop])]), _) =
     1.6        prep (the_list raw_var) [(("", []), [raw_prop])]
     1.7 -        (lthy |> ProofContext.expand_abbrevs false);
     1.8 +        (lthy |> ProofContext.set_expand_abbrevs false);
     1.9      val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
    1.10      val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
    1.11        if x = y then mx
    1.12        else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
    1.13      val lthy' = lthy
    1.14        |> ProofContext.set_syntax_mode mode    (* FIXME !? *)
    1.15 -      |> TermSyntax.abbrevs mode [((x, mx), rhs)]
    1.16 +      |> TermSyntax.abbrev mode ((x, mx), rhs)
    1.17        |> ProofContext.restore_syntax_mode lthy;
    1.18      val _ = print_consts lthy' (K false) [(x, T)]
    1.19    in lthy' end;