--- 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