src/HOL/Predicate_Compile_Examples/ROOT.ML
changeset 40243 3102b27ca03a
parent 40137 9eabcb1bfe50
child 41952 c7297638599b
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Thu Oct 28 15:10:34 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Thu Oct 28 17:28:45 2010 +0200
@@ -12,11 +12,12 @@
 if getenv "EXEC_SWIPL" = "" andalso getenv "EXEC_YAP" = "" then
   (warning "No prolog system found - skipping some example theories"; ())
 else
-  (use_thys [
-    "Code_Prolog_Examples",
-    "Context_Free_Grammar_Example",
-    "Hotel_Example_Prolog",
-    "Lambda_Example",
-    "List_Examples"];
-   Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"]);
-
+  if not (getenv "EXEC_SWIPL" = "") orelse (getenv "SWIPL_VERSION" = "5.10.1") then
+     (use_thys [
+        "Code_Prolog_Examples",
+        "Context_Free_Grammar_Example",
+        "Hotel_Example_Prolog",
+        "Lambda_Example",
+        "List_Examples"];
+      Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"])
+    else (warning "Unsupported SWI-Prolog version - skipping some example theories"; ());