1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 03 12:16:32 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 03 12:31:30 2010 +0200
     1.3 @@ -1726,25 +1726,40 @@
     1.4  
     1.5  (** Axiom extraction/generation **)
     1.6  
     1.7 +fun equationalize t =
     1.8 +  case Logic.strip_imp_concl t of
     1.9 +    @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ _) => t
    1.10 +  | @{const Trueprop} $ t' =>
    1.11 +    @{const Trueprop} $ HOLogic.mk_eq (t', @{const True})
    1.12 +  | _ => t
    1.13 +
    1.14  fun pair_for_prop t =
    1.15    case term_under_def t of
    1.16      Const (s, _) => (s, t)
    1.17    | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
    1.18 +
    1.19  fun def_table_for get ctxt subst =
    1.20    ctxt |> get |> map (pair_for_prop o subst_atomic subst)
    1.21         |> AList.group (op =) |> Symtab.make
    1.22 -fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
    1.23 +
    1.24  fun const_def_table ctxt subst ts =
    1.25    def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst
    1.26    |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
    1.27            (map pair_for_prop ts)
    1.28 +
    1.29 +fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
    1.30  fun const_nondef_table ts =
    1.31    fold (append o paired_with_consts) ts [] |> AList.group (op =) |> Symtab.make
    1.32 -val const_simp_table = def_table_for (map prop_of o Nitpick_Simps.get)
    1.33 -val const_psimp_table = def_table_for (map prop_of o Nitpick_Psimps.get)
    1.34 +
    1.35 +val const_simp_table =
    1.36 +  def_table_for (map (equationalize o prop_of) o Nitpick_Simps.get)
    1.37 +val const_psimp_table =
    1.38 +  def_table_for (map (equationalize o prop_of) o Nitpick_Psimps.get)
    1.39 +
    1.40  fun const_choice_spec_table ctxt subst =
    1.41    map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
    1.42    |> const_nondef_table
    1.43 +
    1.44  fun inductive_intro_table ctxt subst def_table =
    1.45    let val thy = ProofContext.theory_of ctxt in
    1.46      def_table_for
    1.47 @@ -1754,6 +1769,7 @@
    1.48                                    cat = Spec_Rules.Co_Inductive)
    1.49           o Spec_Rules.get) ctxt subst
    1.50    end
    1.51 +
    1.52  fun ground_theorem_table thy =
    1.53    fold ((fn @{const Trueprop} $ t1 =>
    1.54              is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)