src/HOL/Library/refute.ML
changeset 58129 3ec65a7f2b50
parent 58120 a14b8d77b15a
child 58322 f13f6e27d68e
     1.1 --- a/src/HOL/Library/refute.ML	Mon Sep 01 16:34:40 2014 +0200
     1.2 +++ b/src/HOL/Library/refute.ML	Mon Sep 01 17:34:03 2014 +0200
     1.3 @@ -402,7 +402,7 @@
     1.4  fun is_IDT_constructor thy (s, T) =
     1.5    (case body_type T of
     1.6      Type (s', _) =>
     1.7 -      (case Old_Datatype_Data.get_constrs thy s' of
     1.8 +      (case BNF_LFP_Compat.get_constrs thy s' of
     1.9          SOME constrs =>
    1.10            List.exists (fn (cname, cty) =>
    1.11              cname = s andalso Sign.typ_instance thy (T, cty)) constrs
    1.12 @@ -417,7 +417,7 @@
    1.13  fun is_IDT_recursor thy (s, _) =
    1.14    let
    1.15      val rec_names = Symtab.fold (append o #rec_names o snd)
    1.16 -      (Old_Datatype_Data.get_all thy) []
    1.17 +      (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Unfold_Nesting) []
    1.18    in
    1.19      (* I'm not quite sure if checking the name 's' is sufficient, *)
    1.20      (* or if we should also check the type 'T'.                   *)
    1.21 @@ -643,7 +643,6 @@
    1.22    let
    1.23      val thy = Proof_Context.theory_of ctxt
    1.24      val _ = tracing "Adding axioms..."
    1.25 -    val axioms = Theory.all_axioms_of thy
    1.26      fun collect_this_axiom (axname, ax) axs =
    1.27        let
    1.28          val ax' = unfold_defs thy ax
    1.29 @@ -691,7 +690,7 @@
    1.30        (* axiomatic type classes *)
    1.31        | Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs
    1.32        | Type (s, Ts) =>
    1.33 -        (case Old_Datatype_Data.get_info thy s of
    1.34 +        (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.35            SOME _ =>  (* inductive datatype *)
    1.36              (* only collect relevant type axioms for the argument types *)
    1.37              fold collect_type_axioms Ts axs
    1.38 @@ -820,7 +819,7 @@
    1.39        | Type (@{type_name prop}, []) => acc
    1.40        | Type (@{type_name set}, [T1]) => collect_types T1 acc
    1.41        | Type (s, Ts) =>
    1.42 -          (case Old_Datatype_Data.get_info thy s of
    1.43 +          (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.44              SOME info =>  (* inductive datatype *)
    1.45                let
    1.46                  val index = #index info
    1.47 @@ -1015,7 +1014,7 @@
    1.48          (* TODO: no warning needed for /positive/ occurrences of IDTs       *)
    1.49          val maybe_spurious = Library.exists (fn
    1.50              Type (s, _) =>
    1.51 -              (case Old_Datatype_Data.get_info thy s of
    1.52 +              (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.53                  SOME info =>  (* inductive datatype *)
    1.54                    let
    1.55                      val index           = #index info
    1.56 @@ -1741,7 +1740,7 @@
    1.57      val thy = Proof_Context.theory_of ctxt
    1.58      val (typs, terms) = model
    1.59      fun interpret_term (Type (s, Ts)) =
    1.60 -          (case Old_Datatype_Data.get_info thy s of
    1.61 +          (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.62              SOME info =>  (* inductive datatype *)
    1.63                let
    1.64                  (* only recursive IDTs have an associated depth *)
    1.65 @@ -1866,7 +1865,7 @@
    1.66                  HOLogic_empty_set) pairss
    1.67              end
    1.68        | Type (s, Ts) =>
    1.69 -          (case Old_Datatype_Data.get_info thy s of
    1.70 +          (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.71              SOME info =>
    1.72                (case AList.lookup (op =) typs T of
    1.73                  SOME 0 =>
    1.74 @@ -1932,7 +1931,7 @@
    1.75            Const (s, T) =>
    1.76              (case body_type T of
    1.77                Type (s', Ts') =>
    1.78 -                (case Old_Datatype_Data.get_info thy s' of
    1.79 +                (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s' of
    1.80                    SOME info =>  (* body type is an inductive datatype *)
    1.81                      let
    1.82                        val index               = #index info
    1.83 @@ -2404,7 +2403,7 @@
    1.84                  end
    1.85                else
    1.86                  NONE  (* not a recursion operator of this datatype *)
    1.87 -          ) (Old_Datatype_Data.get_all thy) NONE
    1.88 +          ) (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Unfold_Nesting) NONE
    1.89      | _ =>  (* head of term is not a constant *)
    1.90        NONE
    1.91    end;
    1.92 @@ -2838,7 +2837,7 @@
    1.93    in
    1.94      (case T of
    1.95        Type (s, Ts) =>
    1.96 -        (case Old_Datatype_Data.get_info thy s of
    1.97 +        (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.98            SOME info =>  (* inductive datatype *)
    1.99              let
   1.100                val (typs, _)           = model