src/Pure/Isar/specification.ML
changeset 21691 826ab43d43f5
parent 21658 5e31241e1e3c
child 21705 0f3ad56548bc
     1.1 --- a/src/Pure/Isar/specification.ML	Thu Dec 07 16:47:36 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Thu Dec 07 17:58:39 2006 +0100
     1.3 @@ -157,7 +157,7 @@
     1.4          val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
     1.5            if x = y then mx
     1.6            else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
     1.7 -        val lthy2 = lthy1 |> LocalTheory.abbrevs mode [((x, mx), rhs)];
     1.8 +        val lthy2 = lthy1 |> TermSyntax.abbrevs mode [((x, mx), rhs)];
     1.9        in ((x, T), LocalTheory.restore lthy2) end;
    1.10  
    1.11      val (cs, lthy') = lthy
    1.12 @@ -174,7 +174,7 @@
    1.13  (* notation *)
    1.14  
    1.15  fun gen_notation prep_const mode args lthy =
    1.16 -  lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
    1.17 +  lthy |> TermSyntax.notation mode (map (apfst (prep_const lthy)) args);
    1.18  
    1.19  val notation = gen_notation ProofContext.read_const;
    1.20  val notation_i = gen_notation (K I);