| changeset 47698 | 18202d3d5832 |
| parent 47504 | aa1b8a59017f |
| child 47938 | 2924f37cb6b3 |
--- 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)