src/HOL/Nominal/nominal_atoms.ML
changeset 24194 96013f81faef
parent 24162 8dfd5dd65d82
child 24218 fbf1646b267c
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Thu Aug 09 15:52:38 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Aug 09 15:52:42 2007 +0200
     1.3 @@ -456,7 +456,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 ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
     1.8 +        |> AxClass.prove_arity ("Datatype.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 @@ -524,7 +524,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 ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
    1.17 +         |> AxClass.prove_arity ("Datatype.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 @@ -607,7 +607,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 ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
    1.26 +         |> AxClass.prove_arity ("Datatype.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           |> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
    1.29          end) ak_names thy) ak_names thy25;