Protocol_Main breaks simplifier

[dominique-unruh]

In the following code, the by simp command fails, even though test_def is a simplifier rule.
When replacing imports Protocol_Main by imports Main, the by simp command works.
(This problem also occurs when one programatically access the simplifier via libisabelle.)

theory Scratch  
  imports Protocol_Main
begin
  
definition test where "test (x::int) = x"
declare test_def[simp]
  
lemma test2: "a=1 ⟶ test a=1"
  by simp 

[larsrh]

I vaguely remember this problem from updating Leon to Isabelle2016-1. The solution is to reorder imports in Protocol_Main. I'll try to fix this today and push out a new release.

[larsrh]

Fixed in 0.8.3.