src/Pure/Isar/specification.ML
changeset 24676 63eaef3207e1
parent 24624 b8383b1bbae3
child 24724 0df74bb87a13
     1.1 --- a/src/Pure/Isar/specification.ML	Sat Sep 22 17:45:57 2007 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Sat Sep 22 17:45:58 2007 +0200
     1.3 @@ -147,7 +147,7 @@
     1.4    let
     1.5      val ((vars, [(_, [prop])]), _) =
     1.6        prep (the_list raw_var) [(("", []), [raw_prop])]
     1.7 -        (lthy |> ProofContext.set_expand_abbrevs false);
     1.8 +        (lthy |> ProofContext.set_mode ProofContext.mode_abbrev);
     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