# HG changeset patch
# User haftmann
# Date 1328912184 -3600
# Node ID 09ee87ef8b430b6de62431b55ebaf6831e8cb940
# Parent  0db3de1b0cd55bde9adda82569182d1db20aab31
dropped dead code

diff -r 0db3de1b0cd5 -r 09ee87ef8b43 src/HOL/Matrix/Compute_Oracle/compute.ML
--- a/src/HOL/Matrix/Compute_Oracle/compute.ML	Fri Feb 10 23:14:23 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML	Fri Feb 10 23:16:24 2012 +0100
@@ -49,10 +49,9 @@
     val empty : encoding
     val insert : term -> encoding -> int * encoding
     val lookup_code : term -> encoding -> int option
-    val lookup_term : int -> encoding -> term option                                    
+    val lookup_term : int -> encoding -> term option
     val remove_code : int -> encoding -> encoding
     val remove_term : term -> encoding -> encoding
-    val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a                                                      
 end 
 = 
 struct
@@ -76,8 +75,6 @@
 fun remove_term t (e as (count, term2int, int2term)) = 
     (case lookup_code t e of NONE => e | SOME c => (count, Termtab.delete t term2int, Inttab.delete c int2term))
 
-fun fold f (_, term2int, _) = Termtab.fold f term2int
-
 end
 
 exception Make of string;