--- a/src/Pure/Isar/local_theory.ML Fri Sep 29 22:46:59 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML Fri Sep 29 22:47:01 2006 +0200
@@ -25,8 +25,8 @@
val naming: local_theory -> local_theory
val mapping: xstring option -> (local_theory -> local_theory) -> theory -> local_theory * theory
val term_syntax: (Context.generic -> Context.generic) -> local_theory -> local_theory
- val syntax: string * bool -> (string * mixfix) list -> local_theory -> local_theory
- val abbrevs: string * bool -> ((bstring * mixfix) * term) list -> local_theory -> local_theory
+ val syntax: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
+ val abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> local_theory -> local_theory
val consts: ((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory
val consts_restricted: (string * typ -> bool) ->
((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory