src/CTT/ROOT.ML
changeset 4222 d7573d6d0513
parent 3929 3553fcfa2c7e
child 5210 54aaa779b6b4
--- a/src/CTT/ROOT.ML	Wed Nov 12 16:27:13 1997 +0100
+++ b/src/CTT/ROOT.ML	Wed Nov 12 16:28:53 1997 +0100
@@ -15,7 +15,7 @@
 print_depth 1;  
 
 use_thy "CTT";
-use "../Provers/typedsimp.ML";
+use "$ISABELLE_HOME/src/Provers/typedsimp.ML";
 use "rew.ML";
 use_thy "Arith";
 use_thy "Bool";