# HG changeset patch
# User wenzelm
# Date 1427915525 -7200
# Node ID a5591a15112e05c730489b2a6b53d9e45b3a0787
# Parent  91f4f956b1eb59776eacafcdec59ba445670b869
imitate old "intern" semantics for the sake of outdated/unmaintained code, notably relevant for Simpl;

diff -r 91f4f956b1eb -r a5591a15112e src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Apr 01 19:31:28 2015 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed Apr 01 21:12:05 2015 +0200
@@ -173,7 +173,7 @@
 fun mk_free ctxt name =
   if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name
   then
-    let val n' = Variable.intern_fixed ctxt name
+    let val n' = Variable.intern_fixed ctxt name |> perhaps Long_Name.dest_hidden;
     in SOME (Free (n', Proof_Context.infer_type ctxt (n', dummyT))) end
   else NONE