--- a/src/HOL/Lifting.thy Mon Apr 23 16:30:43 2012 +0200
+++ b/src/HOL/Lifting.thy Mon Apr 23 17:18:18 2012 +0200
@@ -12,6 +12,7 @@
"lift_definition" :: thy_goal and
"setup_lifting" :: thy_decl
uses
+ ("Tools/Lifting/lifting_util.ML")
("Tools/Lifting/lifting_info.ML")
("Tools/Lifting/lifting_term.ML")
("Tools/Lifting/lifting_def.ML")
@@ -354,7 +355,7 @@
subsection {* ML setup *}
-text {* Auxiliary data for the lifting package *}
+use "Tools/Lifting/lifting_util.ML"
use "Tools/Lifting/lifting_info.ML"
setup Lifting_Info.setup
--- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Apr 23 16:30:43 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Apr 23 17:18:18 2012 +0200
@@ -18,13 +18,11 @@
structure Lifting_Def: LIFTING_DEF =
struct
-(** Interface and Syntax Setup **)
-
-(* Generation of the code certificate from the rsp theorem *)
+open Lifting_Util
infix 0 MRSL
-fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+(* Generation of the code certificate from the rsp theorem *)
fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
| get_body_types (U, V) = (U, V)
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Apr 23 16:30:43 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Apr 23 17:18:18 2012 +0200
@@ -18,9 +18,9 @@
structure Lifting_Setup: LIFTING_SETUP =
struct
-infix 0 MRSL
+open Lifting_Util
-fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+infix 0 MRSL
exception SETUP_LIFTING_INFR of string
--- a/src/HOL/Tools/Lifting/lifting_term.ML Mon Apr 23 16:30:43 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Mon Apr 23 17:18:18 2012 +0200
@@ -27,6 +27,10 @@
structure Lifting_Term: LIFTING_TERM =
struct
+open Lifting_Util
+
+infix 0 MRSL
+
(* generation of the Quotient theorem *)
exception QUOT_THM_INTERNAL of Pretty.T
@@ -81,10 +85,6 @@
fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
-infix 0 MRSL
-
-fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
-
fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr)
= (rel, abs, rep, cr)
| dest_Quotient t = raise TERM ("dest_Quotient", [t])
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Mon Apr 23 17:18:18 2012 +0200
@@ -0,0 +1,20 @@
+(* Title: HOL/Tools/Lifting/lifting_util.ML
+ Author: Ondrej Kuncar
+
+General-purpose functions used by the Lifting package.
+*)
+
+signature LIFTING_UTIL =
+sig
+ val MRSL: thm list * thm -> thm
+end;
+
+
+structure Lifting_Util: LIFTING_UTIL =
+struct
+
+infix 0 MRSL
+
+fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+
+end;
--- a/src/HOL/Tools/Quotient/quotient_def.ML Mon Apr 23 16:30:43 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Mon Apr 23 17:18:18 2012 +0200
@@ -27,9 +27,9 @@
(* Generation of the code certificate from the rsp theorem *)
-infix 0 MRSL
+open Lifting_Util
-fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+infix 0 MRSL
fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
| get_body_types (U, V) = (U, V)
--- a/src/HOL/Tools/Quotient/quotient_term.ML Mon Apr 23 16:30:43 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Mon Apr 23 17:18:18 2012 +0200
@@ -358,9 +358,9 @@
fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient3})
-infix 0 MRSL
+open Lifting_Util
-fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+infix 0 MRSL
exception NOT_IMPL of string
--- a/src/HOL/Tools/Quotient/quotient_type.ML Mon Apr 23 16:30:43 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Mon Apr 23 17:18:18 2012 +0200
@@ -99,9 +99,9 @@
else
lthy
-infix 0 MRSL
+open Lifting_Util
-fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+infix 0 MRSL
fun define_cr_rel equiv_thm abs_fun lthy =
let