
diff -r b6b6248d4719 -r 914f1f98839c src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Thu Nov 12 16:44:29 2020 +0100
+++ b/src/HOL/ATP.thy	Thu Nov 12 17:42:15 2020 +0100
@@ -137,18 +137,4 @@
 ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close>
 ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close>
 
-ML \<open>
-open ATP_Problem_Generate
-val _ = @{print} (type_enc_of_string Strict "mono_native")
-val _ = @{print} (type_enc_of_string Strict "mono_native_fool")
-val _ = @{print} (type_enc_of_string Strict "poly_native")
-val _ = @{print} (type_enc_of_string Strict "poly_native_fool")
-val _ = @{print} (type_enc_of_string Strict "mono_native?")
-val _ = @{print} (type_enc_of_string Strict "mono_native_fool?")
-val _ = @{print} (type_enc_of_string Strict "erased")
-(* val _ = @{print} (type_enc_of_string Strict "erased_fool") *)
-val _ = @{print} (type_enc_of_string Strict "poly_guards")
-(* val _ = @{print} (type_enc_of_string Strict "poly_guards_fool") *)
-\<close>
-
 end




