src/ZF/ind_syntax.ML

--- a/src/ZF/ind_syntax.ML	Mon Feb 15 15:50:41 2010 +0100
+++ b/src/ZF/ind_syntax.ML	Mon Feb 15 17:17:51 2010 +0100
@@ -65,15 +65,14 @@
   | dest_mem _ = error "Constructor specifications must have the form x:A";
 
 (*read a constructor specification*)
-fun read_construct ctxt (id, sprems, syn) =
+fun read_construct ctxt (id: string, sprems, syn: mixfix) =
     let val prems = map (Syntax.parse_term ctxt #> TypeInfer.constrain FOLogic.oT) sprems
           |> Syntax.check_terms ctxt
         val args = map (#1 o dest_mem) prems
         val T = (map (#2 o dest_Free) args) ---> iT
                 handle TERM _ => error
                     "Bad variable in constructor specification"
-        val name = Syntax.const_name syn id
-    in ((id,T,syn), name, args, prems) end;
+    in ((id,T,syn), id, args, prems) end;
 
 val read_constructs = map o map o read_construct;