# HG changeset patch
# User wenzelm
# Date 1273322483 -7200
# Node ID e9401d2efc5fa768923e6fd08793c027e2e66c70
# Parent  dce592144219ddd9ad594b375d71ac9f54a1bdf1
back-patching via Single_Assignment.var;

diff -r dce592144219 -r e9401d2efc5f src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri May 07 23:44:10 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sat May 08 14:41:23 2010 +0200
@@ -698,21 +698,23 @@
   in (syms, pos) end;
 
 local
-  type operations =
-   {parse_sort: Proof.context -> string -> sort,
-    parse_typ: Proof.context -> string -> typ,
-    parse_term: Proof.context -> string -> term,
-    parse_prop: Proof.context -> string -> term,
-    unparse_sort: Proof.context -> sort -> Pretty.T,
-    unparse_typ: Proof.context -> typ -> Pretty.T,
-    unparse_term: Proof.context -> term -> Pretty.T};
 
-  val operations = Unsynchronized.ref (NONE: operations option);
+type operations =
+ {parse_sort: Proof.context -> string -> sort,
+  parse_typ: Proof.context -> string -> typ,
+  parse_term: Proof.context -> string -> term,
+  parse_prop: Proof.context -> string -> term,
+  unparse_sort: Proof.context -> sort -> Pretty.T,
+  unparse_typ: Proof.context -> typ -> Pretty.T,
+  unparse_term: Proof.context -> term -> Pretty.T};
 
-  fun operation which ctxt x =
-    (case ! operations of
-      NONE => error "Inner syntax operations not yet installed"
-    | SOME ops => which ops ctxt x);
+val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
+
+fun operation which ctxt x =
+  (case Single_Assignment.peek operations of
+    NONE => raise Fail "Inner syntax operations not installed"
+  | SOME ops => which ops ctxt x);
+
 in
 
 val parse_sort = operation #parse_sort;
@@ -723,9 +725,7 @@
 val unparse_typ = operation #unparse_typ;
 val unparse_term = operation #unparse_term;
 
-fun install_operations ops = CRITICAL (fn () =>
-  if is_some (! operations) then error "Inner syntax operations already installed"
-  else operations := SOME ops);
+fun install_operations ops = Single_Assignment.assign operations ops;
 
 end;