trim context for persistent storage;

--- a/src/Tools/nbe.ML	Wed Sep 02 22:14:44 2015 +0200
+++ b/src/Tools/nbe.ML	Wed Sep 02 23:17:18 2015 +0200
@@ -70,7 +70,7 @@
           ^ Syntax.string_of_term_global thy eqn);
     val _ = if the_list (Axclass.class_of_param thy (snd c_c')) = [class] then ()
       else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm);
-  in Triv_Class_Data.map (AList.update (op =) (class, thm)) thy end;
+  in Triv_Class_Data.map (AList.update (op =) (class, Thm.trim_context thm)) thy end;
 
 local