# HG changeset patch
# User blanchet
# Date 1236159819 -3600
# Node ID 179ff9cb160b84a05987dd5a031169fb7c020ad0
# Parent  d8944fd4365e6e30e453f49aa50017f9886cdaba
Made Refute.norm_rhs public, so I can use it in Nitpick.

diff -r d8944fd4365e -r 179ff9cb160b src/HOL/Tools/refute.ML
--- 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) =