# HG changeset patch
# User haftmann
# Date 1328912621 -3600
# Node ID 84f20233d4669ebfcb3f66f77f76abe0354d339a
# Parent  09ee87ef8b430b6de62431b55ebaf6831e8cb940
dropped dead code

diff -r 09ee87ef8b43 -r 84f20233d466 src/HOL/Matrix/Compute_Oracle/am.ML
--- a/src/HOL/Matrix/Compute_Oracle/am.ML	Fri Feb 10 23:16:24 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am.ML	Fri Feb 10 23:23:41 2012 +0100
@@ -15,8 +15,6 @@
    1 to the second last, and so on. *)
 val compile : (guard list * pattern * term) list -> program
 
-val discard : program -> unit
-
 exception Run of string;
 val run : program -> term -> term
 
@@ -66,8 +64,6 @@
 
 fun compile _ = raise Compile "abstract machine stub"
 
-fun discard _ = raise Compile "abstract machine stub"
-
 exception Run of string;
 
 fun run _ _ = raise Run "abstract machine stub"
diff -r 09ee87ef8b43 -r 84f20233d466 src/HOL/Matrix/Compute_Oracle/am_compiler.ML
--- a/src/HOL/Matrix/Compute_Oracle/am_compiler.ML	Fri Feb 10 23:16:24 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_compiler.ML	Fri Feb 10 23:23:41 2012 +0100
@@ -202,9 +202,7 @@
         load_rules "AM_Compiler" "AM_compiled_code" eqs
     end 
 
-fun run prog t = (prog t)
-
-fun discard _ = ()
+fun run prog t = prog t
 
 end
 
diff -r 09ee87ef8b43 -r 84f20233d466 src/HOL/Matrix/Compute_Oracle/am_ghc.ML
--- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Fri Feb 10 23:16:24 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Fri Feb 10 23:23:41 2012 +0100
@@ -320,7 +320,5 @@
         t'
     end
 
-fun discard _ = ()
-
 end
 
diff -r 09ee87ef8b43 -r 84f20233d466 src/HOL/Matrix/Compute_Oracle/am_interpreter.ML
--- a/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML	Fri Feb 10 23:16:24 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML	Fri Feb 10 23:23:41 2012 +0100
@@ -208,6 +208,4 @@
            | _ => raise (Run "internal error in run: weak failed")
      end handle InterruptedExecution state => term_of_clos (resolve state))
 
-fun discard _ = ()
-
 end
diff -r 09ee87ef8b43 -r 84f20233d466 src/HOL/Matrix/Compute_Oracle/am_sml.ML
--- a/src/HOL/Matrix/Compute_Oracle/am_sml.ML	Fri Feb 10 23:16:24 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_sml.ML	Fri Feb 10 23:23:41 2012 +0100
@@ -517,6 +517,4 @@
         compiled_fun (beta (inline t))
     end 
 
-fun discard _ = ()
-
 end
diff -r 09ee87ef8b43 -r 84f20233d466 src/HOL/Matrix/Compute_Oracle/compute.ML
--- a/src/HOL/Matrix/Compute_Oracle/compute.ML	Fri Feb 10 23:16:24 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML	Fri Feb 10 23:23:41 2012 +0100
@@ -20,7 +20,6 @@
     val shyps_of : computer -> sort list
     (* ! *) val update : computer -> thm list -> unit
     (* ! *) val update_with_cache : computer -> term list -> thm list -> unit
-    (* ! *) val discard : computer -> unit
     
     (* ! *) val set_naming : computer -> naming -> unit
     val naming_of : computer -> naming
@@ -323,19 +322,6 @@
 
 fun update computer raw_thms = update_with_cache computer [] raw_thms
 
-fun discard computer =
-    let
-        val _ = 
-            case prog_of computer of
-                ProgBarras p => AM_Interpreter.discard p
-              | ProgBarrasC p => AM_Compiler.discard p
-              | ProgHaskell p => AM_GHC.discard p
-              | ProgSML p => AM_SML.discard p
-        val _ = (ref_of computer) := NONE
-    in
-        ()
-    end 
-                                              
 fun runprog (ProgBarras p) = AM_Interpreter.run p
   | runprog (ProgBarrasC p) = AM_Compiler.run p
   | runprog (ProgHaskell p) = AM_GHC.run p