Made Refute.norm_rhs public, so I can use it in Nitpick.
--- a/src/HOL/Tools/refute.ML Sun Mar 01 18:40:16 2009 +0100
+++ b/src/HOL/Tools/refute.ML Wed Mar 04 10:43:39 2009 +0100
@@ -63,6 +63,7 @@
val close_form : Term.term -> Term.term
val get_classdef : theory -> string -> (string * Term.term) option
+ val norm_rhs : Term.term -> Term.term
val get_def : theory -> string * Term.typ -> (string * Term.term) option
val get_typedef : theory -> Term.typ -> (string * Term.term) option
val is_IDT_constructor : theory -> string * Term.typ -> bool
@@ -548,6 +549,21 @@
end;
(* ------------------------------------------------------------------------- *)
+(* norm_rhs: maps f ?t1 ... ?tn == rhs to %t1...tn. rhs *)
+(* ------------------------------------------------------------------------- *)
+
+ (* Term.term -> Term.term *)
+ fun norm_rhs eqn =
+ let
+ fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
+ | lambda v t = raise TERM ("lambda", [v, t])
+ val (lhs, rhs) = Logic.dest_equals eqn
+ val (_, args) = Term.strip_comb lhs
+ in
+ fold lambda (rev args) rhs
+ end
+
+(* ------------------------------------------------------------------------- *)
(* get_def: looks up the definition of a constant, as created by "constdefs" *)
(* ------------------------------------------------------------------------- *)
@@ -555,16 +571,6 @@
fun get_def thy (s, T) =
let
- (* maps f ?t1 ... ?tn == rhs to %t1...tn. rhs *)
- fun norm_rhs eqn =
- let
- fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
- | lambda v t = raise TERM ("lambda", [v, t])
- val (lhs, rhs) = Logic.dest_equals eqn
- val (_, args) = Term.strip_comb lhs
- in
- fold lambda (rev args) rhs
- end
(* (string * Term.term) list -> (string * Term.term) option *)
fun get_def_ax [] = NONE
| get_def_ax ((axname, ax) :: axioms) =