1.1 --- a/src/HOL/Tools/Function/function_common.ML	Sun Oct 21 22:12:22 2012 +0200
     1.2 +++ b/src/HOL/Tools/Function/function_common.ML	Sun Oct 21 22:31:39 2012 +0200
     1.3 @@ -193,15 +193,13 @@
     1.4  fun import_last_function ctxt =
     1.5    case Item_Net.content (get_function ctxt) of
     1.6      [] => NONE
     1.7 -  | (t, data) :: _ =>
     1.8 +  | (t, _) :: _ =>
     1.9      let
    1.10        val ([t'], ctxt') = Variable.import_terms true [t] ctxt
    1.11      in
    1.12        import_function_data t' ctxt'
    1.13      end
    1.14  
    1.15 -val all_function_data = Item_Net.content o get_function
    1.16 -
    1.17  fun add_function_data (data : info as {fs, termination, ...}) =
    1.18    FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
    1.19    #> store_termination_rule termination