src/HOL/thy_syntax.ML
changeset 3945 ae9c61d69888
parent 3665 3b44fac767f6
child 3980 21ef91734970
     1.1 --- a/src/HOL/thy_syntax.ML	Mon Oct 20 11:14:16 1997 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Mon Oct 20 11:14:55 1997 +0200
     1.3 @@ -143,7 +143,8 @@
     1.4      \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
     1.5      \end;\n\
     1.6      \val dummy = datatypes := Dtype.build_record (thy, " ^
     1.7 -      mk_pair (quote tname, mk_list (map (fst o fst) cons)) ^
     1.8 +      mk_pair ("Sign.intern_tycon (sign_of thy) " ^ quote tname,
     1.9 +        mk_list (map (fst o fst) cons)) ^
    1.10        ", " ^ tname ^ ".induct_tac) :: (!datatypes);\n\
    1.11      \val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\
    1.12      \val dummy = AddIffs " ^ tname ^ ".inject;\n\