src/ZF/Tools/datatype_package.ML
changeset 6093 87bf8c03b169
parent 6092 d9db67970c73
child 6112 5e4871c5136b
     1.1 --- a/src/ZF/Tools/datatype_package.ML	Tue Jan 12 13:54:51 1999 +0100
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Jan 12 15:17:37 1999 +0100
     1.3 @@ -80,7 +80,7 @@
     1.4    val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists)
     1.5  
     1.6    val dummy =	
     1.7 -	writeln ((if (#1 (dest_Const Fp.oper) = "lfp") then "Datatype" 
     1.8 +	writeln ((if (#1 (dest_Const Fp.oper) = "Fixedpt.lfp") then "Datatype" 
     1.9  		  else "Codatatype")
    1.10  		 ^ " definition " ^ big_rec_name)
    1.11  
    1.12 @@ -239,7 +239,7 @@
    1.13    (* Build the new theory *)
    1.14  
    1.15    val need_recursor = 
    1.16 -      (#1 (dest_Const Fp.oper) = "lfp" andalso recursor_typ <> case_typ);
    1.17 +      (#1 (dest_Const Fp.oper) = "Fixedpt.lfp" andalso recursor_typ <> case_typ);
    1.18  
    1.19    fun add_recursor thy = 
    1.20        if need_recursor then
    1.21 @@ -415,7 +415,7 @@
    1.22        val rec_tms = map (readtm sign Ind_Syntax.iT) srec_tms
    1.23        val dom_sum = 
    1.24            if sdom = "" then
    1.25 -	      Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "lfp") rec_tms
    1.26 +	      Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "Fixedpt.lfp") rec_tms
    1.27            else readtm sign Ind_Syntax.iT sdom
    1.28        and con_ty_lists	= Ind_Syntax.read_constructs sign scon_ty_lists
    1.29    in