# HG changeset patch
# User wenzelm
# Date 1441228638 -7200
# Node ID cc5f4b8ac05b625ec4c9f81ffbac049d681d014f
# Parent  50e793295ce147d423482c4a33dad187b8238878
trim context for persistent storage;

diff -r 50e793295ce1 -r cc5f4b8ac05b src/Tools/nbe.ML
--- 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