--- a/src/Tools/permanent_interpretation.ML Thu May 01 09:30:33 2014 +0200
+++ b/src/Tools/permanent_interpretation.ML Thu May 01 09:30:34 2014 +0200
@@ -85,9 +85,10 @@
(* interpretation with permanent registration *)
-fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns lthy =
- generic_interpretation prep_interpretation Element.witness_proof_eqs Local_Theory.notes_kind Local_Theory.subscription
- expression raw_defs raw_eqns lthy
+fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns =
+ Local_Theory.assert_bottom true
+ #> generic_interpretation prep_interpretation Element.witness_proof_eqs
+ Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
in