src/HOL/Tools/BNF/bnf_gfp_grec.ML
changeset 64382 2a75139b5931
parent 63859 dca6fabd8060
child 64627 8d7cb22482e3
equal deleted inserted replaced
64381:59f59f826afd 64382:2a75139b5931
  3110 
  3110 
  3111     val k_As = fold Term.add_tfreesT k_Ts0 [];
  3111     val k_As = fold Term.add_tfreesT k_Ts0 [];
  3112     val _ = (case filter_out (member (op =) As o TFree) k_As of [] => ()
  3112     val _ = (case filter_out (member (op =) As o TFree) k_As of [] => ()
  3113       | k_A :: _ => error ("Cannot have type variable " ^
  3113       | k_A :: _ => error ("Cannot have type variable " ^
  3114           quote (Syntax.string_of_typ lthy (TFree k_A)) ^
  3114           quote (Syntax.string_of_typ lthy (TFree k_A)) ^
  3115           " in the argument types when it does not occur in the result type"));
  3115           " in the argument types when it does not occur as an immediate argument of the result \
       
  3116           \type constructor"));
  3116 
  3117 
  3117     val substDT = Term.typ_subst_atomic (Ds ~~ res_Ds);
  3118     val substDT = Term.typ_subst_atomic (Ds ~~ res_Ds);
  3118 
  3119 
  3119     val old_sig_T0 = Type (old_sig_T_name, As);
  3120     val old_sig_T0 = Type (old_sig_T_name, As);
  3120 
  3121