src/HOL/Tools/Datatype/datatype.ML
changeset 32124 954321008785
parent 31868 edd1f30c0477
child 32172 c4e55f30d527
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Tue Jul 21 15:44:31 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Jul 21 15:52:30 2009 +0200
     1.3 @@ -552,8 +552,7 @@
     1.4              val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
     1.5                  [] => ()
     1.6                | vs => error ("Extra type variables on rhs: " ^ commas vs))
     1.7 -          in (constrs @ [((if #flat_names config then Sign.full_name tmp_thy else
     1.8 -                Sign.full_name_path tmp_thy tname')
     1.9 +          in (constrs @ [(Sign.full_name_path tmp_thy tname'
    1.10                    (Binding.map_name (Syntax.const_name mx') cname),
    1.11                     map (dtyp_of_typ new_dts) cargs')],
    1.12                constr_syntax' @ [(cname, mx')], sorts'')