src/Pure/Isar/specification.ML

     val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
       if x = y then mx
       else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
     val lthy' = lthy
       |> ProofContext.set_syntax_mode mode    (* FIXME !? *)
-      |> TermSyntax.abbrev mode ((x, mx), rhs)
+      |> LocalTheory.abbrev mode ((x, mx), rhs)
       |> ProofContext.restore_syntax_mode lthy;
     val _ = print_consts lthy' (K false) [(x, T)]
   in lthy' end;
 
 val abbreviation = gen_abbrev read_specification;

 
 
 (* notation *)
 
 fun gen_notation prep_const mode args lthy =
-  lthy |> TermSyntax.notation mode (map (apfst (prep_const lthy)) args);
+  lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
 
 val notation = gen_notation ProofContext.read_const;
 val notation_i = gen_notation (K I);