# HG changeset patch
# User kuncar
# Date 1335194298 -7200
# Node ID 18202d3d58321936226ac578d75326455340548f
# Parent  0622929ca66e85ffa99fb97d913d61a5bb156fc6
move MRSL to a separate file

diff -r 0622929ca66e -r 18202d3d5832 src/HOL/Lifting.thy
--- 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
diff -r 0622929ca66e -r 18202d3d5832 src/HOL/Tools/Lifting/lifting_def.ML
--- 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)
diff -r 0622929ca66e -r 18202d3d5832 src/HOL/Tools/Lifting/lifting_setup.ML
--- 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
 
diff -r 0622929ca66e -r 18202d3d5832 src/HOL/Tools/Lifting/lifting_term.ML
--- 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])
diff -r 0622929ca66e -r 18202d3d5832 src/HOL/Tools/Lifting/lifting_util.ML
--- /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;
diff -r 0622929ca66e -r 18202d3d5832 src/HOL/Tools/Quotient/quotient_def.ML
--- 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)
diff -r 0622929ca66e -r 18202d3d5832 src/HOL/Tools/Quotient/quotient_term.ML
--- 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
 
diff -r 0622929ca66e -r 18202d3d5832 src/HOL/Tools/Quotient/quotient_type.ML
--- 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