1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Aug 03 12:16:32 2010 +0200
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Aug 03 12:31:30 2010 +0200
     1.3 @@ -2585,7 +2585,7 @@
     1.4  and \textbf{nominal\_\allowbreak primrec} packages, this corresponds to the
     1.5  \textit{simps} rules. The equations must be of the form
     1.6  
     1.7 -\qquad $c~t_1~\ldots\ t_n \,=\, u.$
     1.8 +\qquad $c~t_1~\ldots\ t_n \;\bigl[{=}\; u\bigr].$
     1.9  
    1.10  \flushitem{\textit{nitpick\_psimp}}
    1.11  
    1.12 @@ -2595,7 +2595,7 @@
    1.13  corresponds to the \textit{psimps} rules. The conditional equations must be of
    1.14  the form
    1.15  
    1.16 -\qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,=\, u$.
    1.17 +\qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \;\bigl[{=}\; u\bigr]$.
    1.18  
    1.19  \flushitem{\textit{nitpick\_choice\_spec}}
    1.20  

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 03 12:16:32 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 03 12:31:30 2010 +0200
     2.3 @@ -1726,25 +1726,40 @@
     2.4  
     2.5  (** Axiom extraction/generation **)
     2.6  
     2.7 +fun equationalize t =
     2.8 +  case Logic.strip_imp_concl t of
     2.9 +    @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ _ $ _) => t
    2.10 +  | @{const Trueprop} $ t' =>
    2.11 +    @{const Trueprop} $ HOLogic.mk_eq (t', @{const True})
    2.12 +  | _ => t
    2.13 +
    2.14  fun pair_for_prop t =
    2.15    case term_under_def t of
    2.16      Const (s, _) => (s, t)
    2.17    | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
    2.18 +
    2.19  fun def_table_for get ctxt subst =
    2.20    ctxt |> get |> map (pair_for_prop o subst_atomic subst)
    2.21         |> AList.group (op =) |> Symtab.make
    2.22 -fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
    2.23 +
    2.24  fun const_def_table ctxt subst ts =
    2.25    def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst
    2.26    |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
    2.27            (map pair_for_prop ts)
    2.28 +
    2.29 +fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
    2.30  fun const_nondef_table ts =
    2.31    fold (append o paired_with_consts) ts [] |> AList.group (op =) |> Symtab.make
    2.32 -val const_simp_table = def_table_for (map prop_of o Nitpick_Simps.get)
    2.33 -val const_psimp_table = def_table_for (map prop_of o Nitpick_Psimps.get)
    2.34 +
    2.35 +val const_simp_table =
    2.36 +  def_table_for (map (equationalize o prop_of) o Nitpick_Simps.get)
    2.37 +val const_psimp_table =
    2.38 +  def_table_for (map (equationalize o prop_of) o Nitpick_Psimps.get)
    2.39 +
    2.40  fun const_choice_spec_table ctxt subst =
    2.41    map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
    2.42    |> const_nondef_table
    2.43 +
    2.44  fun inductive_intro_table ctxt subst def_table =
    2.45    let val thy = ProofContext.theory_of ctxt in
    2.46      def_table_for
    2.47 @@ -1754,6 +1769,7 @@
    2.48                                    cat = Spec_Rules.Co_Inductive)
    2.49           o Spec_Rules.get) ctxt subst
    2.50    end
    2.51 +
    2.52  fun ground_theorem_table thy =
    2.53    fold ((fn @{const Trueprop} $ t1 =>
    2.54              is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)