Change of type for proof-script-span-context-menu-extensions

3 files changed, 4 insertions, 11 deletions

diff --git a/isar/Example-Tokens.thy b/isar/Example-Tokens.thy
index 6d2f69ec..8856eba4 100644
--- a/isar/Example-Tokens.thy
+++ b/isar/Example-Tokens.thy
@@ -13,21 +13,12 @@ theory "Example-Xsym" imports Main begin
 
 text {* Proper proof text -- \<^bitalic>naive version\<^eitalic>. *}
 
-theorem and_comms: "\<phi> \<and> \<psi> \<longrightarrow> \<psi> \<and> \<phi>"
-proof
-  assume "\<phi> \<and> \<psi>"
-  then show "\<psi> \<and> \<phi>"
-  proof
-    assume \<psi> and \<phi>
-    then show ?thesis ..
- qed
-qed
-
 text {* \<^bbold>Unstructured\<^ebold> proof script. *}
 
 theorem "\<phi>\<^isub>\<alpha> \<and> \<phi>\<^isub>\<beta> \<longrightarrow> \<phi>\<^isub>\<beta> \<and> \<phi>\<^isub>\<alpha>"
   apply (rule impI)
   apply (erule conjE)
+  
   apply (rule conjI)
   apply assumption
   apply assumption
diff --git a/isar/Example.thy b/isar/Example.thy
index 720e5480..a826cae8 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -19,6 +19,8 @@ proof
  qed
 qed
 
+(* quite nice I think but what if I type here? *)
+
 text {* Unstructured proof script. *}
 
 theorem  "A & B --> B & A"
diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el
index f66e41ba..ec405b13 100644
--- a/isar/isabelle-system.el
+++ b/isar/isabelle-system.el
@@ -342,7 +342,7 @@ for you, you should disable this behaviour."
 ;;
 
 (defun isabelle-create-span-menu (span idiom name)
-  (if (string-equal idiom "proof")
+  (if (eq idiom 'proof)
       (let ((thm (span-property span 'name)))
 	(list (vector
 	       "Visualise dependencies"