# HG changeset patch
# User wenzelm
# Date 1350851499 -7200
# Node ID cf4c03c019e59ace7009f2f6b9814a4ab75ba8a2
# Parent  ee25a04fa06a0c9a79e2f3c249f99ef5fc0d50d9
removed dead code;

diff -r ee25a04fa06a -r cf4c03c019e5 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sun Oct 21 22:12:22 2012 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Sun Oct 21 22:31:39 2012 +0200
@@ -193,15 +193,13 @@
 fun import_last_function ctxt =
   case Item_Net.content (get_function ctxt) of
     [] => NONE
-  | (t, data) :: _ =>
+  | (t, _) :: _ =>
     let
       val ([t'], ctxt') = Variable.import_terms true [t] ctxt
     in
       import_function_data t' ctxt'
     end
 
-val all_function_data = Item_Net.content o get_function
-
 fun add_function_data (data : info as {fs, termination, ...}) =
   FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
   #> store_termination_rule termination