# HG changeset patch # User wenzelm # Date 880039445 -3600 # Node ID e4113a68288312b3d0662bf5b7fa3a7189d8b506 # Parent e20b9fd85811d13d762331bc3ec1098f8111ea60 $ISABELLE_HOME/src; diff -r e20b9fd85811 -r e4113a682883 src/ZF/ROOT.ML --- a/src/ZF/ROOT.ML Thu Nov 20 15:48:32 1997 +0100 +++ b/src/ZF/ROOT.ML Thu Nov 20 16:24:05 1997 +0100 @@ -30,7 +30,7 @@ print_depth 1; (*Add user sections for inductive/datatype definitions*) -use "../Pure/section_utils.ML"; +use "$ISABELLE_HOME/src/Pure/section_utils.ML"; use "thy_syntax.ML"; use_thy "Let";