# HG changeset patch
# User haftmann
# Date 1328911977 -3600
# Node ID 55fea563fbee7db187884cfcbe7a24e31fc8959c
# Parent  faf233c4a404e1a2bf14e0b9307e5048a973c6bb
dropped dead code

diff -r faf233c4a404 -r 55fea563fbee src/HOL/Matrix/Compute_Oracle/am.ML
--- a/src/HOL/Matrix/Compute_Oracle/am.ML	Fri Feb 10 23:06:21 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am.ML	Fri Feb 10 23:12:57 2012 +0100
@@ -13,7 +13,7 @@
 
 (* The de-Bruijn index 0 occurring on the right hand side refers to the LAST pattern variable, when traversing the pattern from left to right,
    1 to the second last, and so on. *)
-val compile : pattern list -> (int -> int option) -> (guard list * pattern * term) list -> program
+val compile : (guard list * pattern * term) list -> program
 
 val discard : program -> unit
 
diff -r faf233c4a404 -r 55fea563fbee src/HOL/Matrix/Compute_Oracle/am_compiler.ML
--- a/src/HOL/Matrix/Compute_Oracle/am_compiler.ML	Fri Feb 10 23:06:21 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_compiler.ML	Fri Feb 10 23:12:57 2012 +0100
@@ -190,7 +190,7 @@
           | SOME r => (compiled_rewriter := NONE; r)
     end 
 
-fun compile _ _ eqs = 
+fun compile eqs = 
     let
         val _ = if exists (fn (a,_,_) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
         val eqs = map (fn (_,b,c) => (b,c)) eqs
diff -r faf233c4a404 -r 55fea563fbee src/HOL/Matrix/Compute_Oracle/am_ghc.ML
--- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Fri Feb 10 23:06:21 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Fri Feb 10 23:12:57 2012 +0100
@@ -216,7 +216,7 @@
     
 fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false)
 
-fun compile _ _ eqs = 
+fun compile eqs = 
     let
         val _ = if exists (fn (a,_,_) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
         val eqs = map (fn (_,b,c) => (b,c)) eqs
diff -r faf233c4a404 -r 55fea563fbee src/HOL/Matrix/Compute_Oracle/am_interpreter.ML
--- a/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML	Fri Feb 10 23:06:21 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML	Fri Feb 10 23:12:57 2012 +0100
@@ -100,7 +100,7 @@
   | check_freevars free (Abs m) = check_freevars (free+1) m
   | check_freevars free (Computed t) = check_freevars free t
 
-fun compile _ _ eqs =
+fun compile eqs =
     let
         fun check p r = if check_freevars p r then () else raise Compile ("unbound variables in rule") 
         fun check_guard p (Guard (a,b)) = (check p a; check p b) 
diff -r faf233c4a404 -r 55fea563fbee src/HOL/Matrix/Compute_Oracle/am_sml.ML
--- a/src/HOL/Matrix/Compute_Oracle/am_sml.ML	Fri Feb 10 23:06:21 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_sml.ML	Fri Feb 10 23:12:57 2012 +0100
@@ -490,7 +490,7 @@
 
 fun use_source src = use_text ML_Env.local_context (1, "") false src
     
-fun compile _ _ eqs = 
+fun compile eqs = 
     let
         val guid = get_guid ()
         val code = Real.toString (random ())
diff -r faf233c4a404 -r 55fea563fbee src/HOL/Matrix/Compute_Oracle/compute.ML
--- a/src/HOL/Matrix/Compute_Oracle/compute.ML	Fri Feb 10 23:06:21 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML	Fri Feb 10 23:12:57 2012 +0100
@@ -297,24 +297,14 @@
                 (encoding, p::cache_patterns)
             end
         
-        val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
-
-        fun arity (Type ("fun", [_, b])) = 1 + arity b
-          | arity _ = 0
-
-        fun make_arity (Const (s, _), i) tab = 
-            (Inttab.update (i, arity (Sign.the_const_type thy s)) tab handle TYPE _ => tab)
-          | make_arity _ tab = tab
-
-        val const_arity_tab = Encode.fold make_arity encoding Inttab.empty
-        fun const_arity x = Inttab.lookup const_arity_tab x 
+        val (encoding, _) = fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
 
         val prog = 
             case machine of 
-                BARRAS => ProgBarras (AM_Interpreter.compile cache_patterns const_arity rules)
-              | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile cache_patterns const_arity rules)
-              | HASKELL => ProgHaskell (AM_GHC.compile cache_patterns const_arity rules)
-              | SML => ProgSML (AM_SML.compile cache_patterns const_arity rules)
+                BARRAS => ProgBarras (AM_Interpreter.compile rules)
+              | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile rules)
+              | HASKELL => ProgHaskell (AM_GHC.compile rules)
+              | SML => ProgSML (AM_SML.compile rules)
 
         fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))