# HG changeset patch
# User haftmann
# Date 1328915190 -3600
# Node ID dcc575b3084277d0bd6cadcf28bf06cffcea2a9d
# Parent  9673597c1b92ada636ea5acab5dcd2fb8939b4c1
tuned

diff -r 9673597c1b92 -r dcc575b30842 src/HOL/Matrix/Compute_Oracle/am_sml.ML
--- a/src/HOL/Matrix/Compute_Oracle/am_sml.ML	Fri Feb 10 23:56:09 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_sml.ML	Sat Feb 11 00:06:30 2012 +0100
@@ -98,50 +98,47 @@
 
 (* Remove all rules that are just parameterless rewrites. This is necessary because SML does not allow functions with no parameters. *)
 fun inline_rules rules =
-    let
-        fun term_contains_const c (App (a, b)) = term_contains_const c a orelse term_contains_const c b
-          | term_contains_const c (Abs m) = term_contains_const c m
-          | term_contains_const c (Var _) = false
-          | term_contains_const c (Const c') = (c = c')
-        fun find_rewrite [] = NONE
-          | find_rewrite ((prems, PConst (c, []), r) :: _) = 
-            if check_freevars 0 r then 
-                if term_contains_const c r then 
-                    raise Compile "parameterless rewrite is caught in cycle"
-                else if not (null prems) then
-                    raise Compile "parameterless rewrite may not be guarded"
-                else
-                    SOME (c, r) 
-            else raise Compile "unbound variable on right hand side or guards of rule"
-          | find_rewrite (_ :: rules) = find_rewrite rules
-        fun remove_rewrite _ [] = []
-          | remove_rewrite (cr as (c,r)) ((rule as (prems', PConst (c', args), r'))::rules) = 
-            (if c = c' then 
-                 if null args andalso r = r' andalso null (prems') then 
-                     remove_rewrite cr rules 
-                 else raise Compile "incompatible parameterless rewrites found"
-             else
-                 rule :: (remove_rewrite cr rules))
-          | remove_rewrite cr (r::rs) = r::(remove_rewrite cr rs)
-        fun pattern_contains_const c (PConst (c', args)) = (c = c' orelse exists (pattern_contains_const c) args)
-          | pattern_contains_const c (PVar) = false
-        fun inline_rewrite (ct as (c, _)) (prems, p, r) = 
-            if pattern_contains_const c p then 
-                raise Compile "parameterless rewrite cannot be used in pattern"
-            else (map (fn (Guard (a,b)) => Guard (subst_const ct a, subst_const ct b)) prems, p, subst_const ct r)
-        fun inline inlined rules =
-            (case find_rewrite rules of 
-                 NONE => (Inttab.make inlined, rules)
-               | SOME ct => 
-                 let
-                     val rules = map (inline_rewrite ct) (remove_rewrite ct rules)
-                     val inlined =  ct :: (map (fn (c', r) => (c', subst_const ct r)) inlined)
-                 in
-                     inline inlined rules
-                 end)           
-    in
-        inline [] rules         
-    end
+  let
+    fun term_contains_const c (App (a, b)) = term_contains_const c a orelse term_contains_const c b
+      | term_contains_const c (Abs m) = term_contains_const c m
+      | term_contains_const c (Var _) = false
+      | term_contains_const c (Const c') = (c = c')
+    fun find_rewrite [] = NONE
+      | find_rewrite ((prems, PConst (c, []), r) :: _) = 
+          if check_freevars 0 r then 
+            if term_contains_const c r then 
+              raise Compile "parameterless rewrite is caught in cycle"
+            else if not (null prems) then
+              raise Compile "parameterless rewrite may not be guarded"
+            else
+              SOME (c, r) 
+          else raise Compile "unbound variable on right hand side or guards of rule"
+      | find_rewrite (_ :: rules) = find_rewrite rules
+    fun remove_rewrite _ [] = []
+      | remove_rewrite (cr as (c, r)) ((rule as (prems', PConst (c', args), r')) :: rules) = 
+          if c = c' then 
+            if null args andalso r = r' andalso null prems' then remove_rewrite cr rules 
+            else raise Compile "incompatible parameterless rewrites found"
+          else
+            rule :: remove_rewrite cr rules
+      | remove_rewrite cr (r :: rs) = r :: remove_rewrite cr rs
+    fun pattern_contains_const c (PConst (c', args)) = c = c' orelse exists (pattern_contains_const c) args
+      | pattern_contains_const c (PVar) = false
+    fun inline_rewrite (ct as (c, _)) (prems, p, r) = 
+        if pattern_contains_const c p then 
+          raise Compile "parameterless rewrite cannot be used in pattern"
+        else (map (fn (Guard (a, b)) => Guard (subst_const ct a, subst_const ct b)) prems, p, subst_const ct r)
+    fun inline inlined rules =
+      case find_rewrite rules of 
+          NONE => (Inttab.make inlined, rules)
+        | SOME ct => 
+            let
+              val rules = map (inline_rewrite ct) (remove_rewrite ct rules)
+              val inlined = ct :: (map o apsnd) (subst_const ct) inlined
+            in inline inlined rules end
+  in
+    inline [] rules
+  end
 
 
 (*