src/HOL/Tools/inductive_package.ML
changeset 23881 851c74f1bb69
parent 23762 24eef53a9ad3
child 24039 273698405054
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jul 20 14:28:05 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Jul 20 14:28:25 2007 +0200
     1.3 @@ -181,7 +181,7 @@
     1.4      case concl of
     1.5        Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
     1.6      | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
     1.7 -    | _ $ (Const ("Orderings.ord_class.less_eq", _) $ _ $ _) =>
     1.8 +    | _ $ (Const ("HOL.ord_class.less_eq", _) $ _ $ _) =>
     1.9        [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
    1.10           (resolve_tac [le_funI, le_boolI'])) thm))]
    1.11      | _ => [thm]
    1.12 @@ -554,7 +554,7 @@
    1.13           (make_bool_args HOLogic.mk_not I bs i)) preds));
    1.14  
    1.15      val ind_concl = HOLogic.mk_Trueprop
    1.16 -      (HOLogic.mk_binrel "Orderings.ord_class.less_eq" (rec_const, ind_pred));
    1.17 +      (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
    1.18  
    1.19      val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
    1.20