From 0914a1fc5cfa6d5db0cb9d1cd1b7c869b2ade030 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Fri, 24 Aug 2018 22:02:04 +0200
Subject: [PATCH] A little cleanup.

---
 Isa_DOF.thy | 19 +------------------
 1 file changed, 1 insertion(+), 18 deletions(-)

diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index d50e8f0c..8f27b370 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -485,11 +485,6 @@ val attributes_upd =
          (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute_upd))) []))
      --| Parse.$$$ "]"
 
-val SPY = Unsynchronized.ref ([]:((term * Position.T) * term) list) 
-
-val SPY2 = Unsynchronized.ref ([]:Symbol_Pos.T list);
-
-val SPY3 = Unsynchronized.ref ("");
 
 
 fun cid_2_cidType cid_long thy =
@@ -775,21 +770,11 @@ val _ = theorem @{command_keyword proposition} false "proposition";
 val _ = theorem @{command_keyword schematic_goal} true "schematic goal"; *)
 
 in end\<close>  
-  
-
-assert "True"  
-  
-  
+    
 (* experiments >>> *)
   
 text*[sdf] {* f @{thm refl}*}  
 text*[sdfg] {* fg @{thm refl}*}  
-ML{* ODL_Command_Parser.SPY3; 
-(* produces: ref "fg \\isa{<markup>\\ {\\isacharequal}\\ <markup>}": string ref *)
-(* This proves that  Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks actually
-PRODUCES strings in which the antiquotations were expanded. *)
-*} 
-(* <<< experiments *)  
   
 section{* Syntax for Ontological Antiquotations (the '' View'' Part II) *}
   
@@ -1029,8 +1014,6 @@ end (* struct *)
 
 text*[xxxy] {* dd @{docitem_ref \<open>sdfg\<close>}  @{thm refl}*}    
   
-ML{* ODL_Command_Parser.SPY3; *}  
-
    
 section{* Library of Standard Text Ontology *}