src/HOL/Statespace/state_space.ML

        bool -> Proof.context -> string -> term -> term -> term
     val update_tr : Proof.context -> term list -> term
     val update_tr' : Proof.context -> term list -> term
   end;
 
-
 structure StateSpace: STATE_SPACE =
 struct
 
 (* Theorems *)
 

         in (ctxt',thm)
         end)
 
     val attr = Attrib.internal type_attr;
 
-    val assumes = Element.Assumes [((dist_thm_name,[attr]),
+    val assumes = Element.Assumes [((Name.binding dist_thm_name,[attr]),
                     [(HOLogic.Trueprop $
                       (Const ("DistinctTreeProver.all_distinct",
                                  Type ("DistinctTreeProver.tree",[nameT]) --> HOLogic.boolT) $
                       DistinctTreeProver.mk_tree (fn n => Free (n,nameT)) nameT
                                 (sort fast_string_ord all_comps)),

        (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init thy))) T;
    val fixestate = (case state_type of
          NONE => []
        | SOME s =>
           let
-	    val fx = Element.Fixes [(s,SOME (string_of_typ stateT),NoSyn)];
+	    val fx = Element.Fixes [(Name.binding s,SOME (string_of_typ stateT),NoSyn)];
             val cs = Element.Constrains
                        (map (fn (n,T) =>  (n,string_of_typ T))
                          ((map (fn (n,_) => (n,nameT)) all_comps) @
                           constrains))
           in [fx,cs] end