src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 46086 096697aec8a7
parent 46083 efeaa79f021b
child 46088 948bef826443
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:17 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:18 2012 +0100
     1.3 @@ -1815,12 +1815,17 @@
     1.4  
     1.5  (** Axiom extraction/generation **)
     1.6  
     1.7 -fun extensional_equal j (Type (@{type_name fun}, [dom_T, ran_T])) t1 t2 =
     1.8 -    let val var_t = Var (("x", j), dom_T) in
     1.9 +fun extensional_equal j T t1 t2 =
    1.10 +  if is_fun_type T orelse is_set_like_type T then
    1.11 +    let
    1.12 +      val dom_T = pseudo_domain_type T
    1.13 +      val ran_T = pseudo_range_type T
    1.14 +      val var_t = Var (("x", j), dom_T)
    1.15 +    in
    1.16        extensional_equal (j + 1) ran_T (betapply (t1, var_t))
    1.17                          (betapply (t2, var_t))
    1.18      end
    1.19 -  | extensional_equal _ T t1 t2 =
    1.20 +  else
    1.21      Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2
    1.22  
    1.23  fun equationalize_term ctxt tag t =
    1.24 @@ -1837,7 +1842,7 @@
    1.25            @{const Trueprop} $ HOLogic.mk_eq (t', @{const True})
    1.26          | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
    1.27            @{const Trueprop} $ extensional_equal j T t1 t2
    1.28 -        | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation" ^
    1.29 +        | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^
    1.30                           quote (Syntax.string_of_term ctxt t) ^ ".");
    1.31                  raise SAME ()))
    1.32      |> SOME