--- a/src/HOL/Matrix/MatrixLP.ML	Fri Sep 03 17:46:47 2004 +0200
+++ b/src/HOL/Matrix/MatrixLP.ML	Fri Sep 03 20:20:44 2004 +0200
@@ -73,9 +73,9 @@
 	removeTrue th
     end
 
-fun float2real (x,y) = (Real.fromInt x) * (Math.pow (2.0, Real.fromInt y))
+end
 
-end
+fun float2real (x,y) = (Real.fromInt x) * (Math.pow (2.0, Real.fromInt y))
 
 val result = ref ([]:thm list)