# 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