src/HOL/Nominal/nominal_atoms.ML
changeset 30235 58d147683393
parent 30086 2023fb9fbf31
child 30345 76fd85bbf139
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Mar 03 17:05:18 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Mar 04 10:47:20 2009 +0100
     1.3 @@ -539,7 +539,7 @@
     1.4          thy
     1.5          |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
     1.6          |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
     1.7 -        |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
     1.8 +        |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
     1.9          |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
    1.10          |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
    1.11          |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    1.12 @@ -606,7 +606,7 @@
    1.13           |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    1.14                                       (fs_proof fs_thm_nprod) 
    1.15           |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
    1.16 -         |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
    1.17 +         |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
    1.18          end) ak_names thy20;
    1.19  
    1.20         (********  cp_<ak>_<ai> class instances  ********)
    1.21 @@ -687,7 +687,7 @@
    1.22           |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
    1.23           |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
    1.24           |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
    1.25 -         |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
    1.26 +         |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
    1.27           |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
    1.28          end) ak_names thy) ak_names thy25;
    1.29