src/HOL/Library/refute.ML
changeset 58354 04ac60da613e
parent 58322 f13f6e27d68e
child 58825 2065f49da190
     1.1 --- a/src/HOL/Library/refute.ML	Tue Sep 16 19:23:37 2014 +0200
     1.2 +++ b/src/HOL/Library/refute.ML	Wed Sep 17 08:23:53 2014 +0200
     1.3 @@ -416,8 +416,7 @@
     1.4  
     1.5  fun is_IDT_recursor thy (s, _) =
     1.6    let
     1.7 -    val rec_names = Symtab.fold (append o #rec_names o snd)
     1.8 -      (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Unfold_Nesting) []
     1.9 +    val rec_names = Symtab.fold (append o #rec_names o snd) (BNF_LFP_Compat.get_all thy []) []
    1.10    in
    1.11      (* I'm not quite sure if checking the name 's' is sufficient, *)
    1.12      (* or if we should also check the type 'T'.                   *)
    1.13 @@ -690,7 +689,7 @@
    1.14        (* axiomatic type classes *)
    1.15        | Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs
    1.16        | Type (s, Ts) =>
    1.17 -        (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.18 +        (case BNF_LFP_Compat.get_info thy [] s of
    1.19            SOME _ =>  (* inductive datatype *)
    1.20              (* only collect relevant type axioms for the argument types *)
    1.21              fold collect_type_axioms Ts axs
    1.22 @@ -819,7 +818,7 @@
    1.23        | Type (@{type_name prop}, []) => acc
    1.24        | Type (@{type_name set}, [T1]) => collect_types T1 acc
    1.25        | Type (s, Ts) =>
    1.26 -          (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.27 +          (case BNF_LFP_Compat.get_info thy [] s of
    1.28              SOME info =>  (* inductive datatype *)
    1.29                let
    1.30                  val index = #index info
    1.31 @@ -1014,7 +1013,7 @@
    1.32          (* TODO: no warning needed for /positive/ occurrences of IDTs       *)
    1.33          val maybe_spurious = Library.exists (fn
    1.34              Type (s, _) =>
    1.35 -              (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.36 +              (case BNF_LFP_Compat.get_info thy [] s of
    1.37                  SOME info =>  (* inductive datatype *)
    1.38                    let
    1.39                      val index           = #index info
    1.40 @@ -1740,7 +1739,7 @@
    1.41      val thy = Proof_Context.theory_of ctxt
    1.42      val (typs, terms) = model
    1.43      fun interpret_term (Type (s, Ts)) =
    1.44 -          (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.45 +          (case BNF_LFP_Compat.get_info thy [] s of
    1.46              SOME info =>  (* inductive datatype *)
    1.47                let
    1.48                  (* only recursive IDTs have an associated depth *)
    1.49 @@ -1865,7 +1864,7 @@
    1.50                  HOLogic_empty_set) pairss
    1.51              end
    1.52        | Type (s, Ts) =>
    1.53 -          (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.54 +          (case BNF_LFP_Compat.get_info thy [] s of
    1.55              SOME info =>
    1.56                (case AList.lookup (op =) typs T of
    1.57                  SOME 0 =>
    1.58 @@ -1931,7 +1930,7 @@
    1.59            Const (s, T) =>
    1.60              (case body_type T of
    1.61                Type (s', Ts') =>
    1.62 -                (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s' of
    1.63 +                (case BNF_LFP_Compat.get_info thy [] s' of
    1.64                    SOME info =>  (* body type is an inductive datatype *)
    1.65                      let
    1.66                        val index               = #index info
    1.67 @@ -2403,7 +2402,7 @@
    1.68                  end
    1.69                else
    1.70                  NONE  (* not a recursion operator of this datatype *)
    1.71 -          ) (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Unfold_Nesting) NONE
    1.72 +          ) (BNF_LFP_Compat.get_all thy []) NONE
    1.73      | _ =>  (* head of term is not a constant *)
    1.74        NONE
    1.75    end;
    1.76 @@ -2837,7 +2836,7 @@
    1.77    in
    1.78      (case T of
    1.79        Type (s, Ts) =>
    1.80 -        (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.81 +        (case BNF_LFP_Compat.get_info thy [] s of
    1.82            SOME info =>  (* inductive datatype *)
    1.83              let
    1.84                val (typs, _)           = model
    1.85 @@ -3003,4 +3002,3 @@
    1.86          in thy' end)));
    1.87  
    1.88  end;
    1.89 -