src/Pure/axclass.ML
changeset 15531 08c8dad8e399
parent 15457 1fbd4aba46e3
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/axclass.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/axclass.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4  val is_def = Logic.is_equals o #prop o rep_thm;
     1.5  
     1.6  fun witnesses thy names thms =
     1.7 -  PureThy.get_thmss thy (map (rpair None) names) @ thms @ filter is_def (map snd (axioms_of thy));
     1.8 +  PureThy.get_thmss thy (map (rpair NONE) names) @ thms @ filter is_def (map snd (axioms_of thy));
     1.9  
    1.10  
    1.11  
    1.12 @@ -201,8 +201,8 @@
    1.13  
    1.14  fun get_axclass_info thy c =
    1.15    (case lookup_axclass_info_sg (Theory.sign_of thy) c of
    1.16 -    None => error ("Unknown axclass " ^ quote c)
    1.17 -  | Some info => info);
    1.18 +    NONE => error ("Unknown axclass " ^ quote c)
    1.19 +  | SOME info => info);
    1.20  
    1.21  fun put_axclass_info c info thy =
    1.22    thy |> AxclassesData.put (Symtab.update ((c, info), AxclassesData.get thy));
    1.23 @@ -391,8 +391,8 @@
    1.24          prove_arity sign (t, Ss, c) wthms usr_tac);
    1.25    in add_arity_thms (map prove cs) thy end;
    1.26  
    1.27 -fun sane_inst_subclass prep sub tac = ext_inst_subclass prep sub [] [] (Some tac);
    1.28 -fun sane_inst_arity prep arity tac = ext_inst_arity prep arity [] [] (Some tac);
    1.29 +fun sane_inst_subclass prep sub tac = ext_inst_subclass prep sub [] [] (SOME tac);
    1.30 +fun sane_inst_arity prep arity tac = ext_inst_arity prep arity [] [] (SOME tac);
    1.31  
    1.32  val add_inst_subclass_x = ext_inst_subclass read_classrel;
    1.33  val add_inst_subclass = sane_inst_subclass read_classrel;