test/Tools/isac/ADDTESTS/file-depend/3knowledge/Foo_Know111.thy
author Walther Neuper <neuper@ist.tugraz.at>
Thu, 26 Aug 2010 10:03:53 +0200
branchisac-update-Isa09-2
changeset 37949 aaf528d3ebd5
parent 37946 a28b5fc129b7
child 37965 9c11005c33b8
permissions -rw-r--r--
messed file dependencies.

The mess becomes apparent when unduly simplifying to
'theory Atools imports Complex_Main'
(*theory Atools imports Descript Typefix begin ...WOULD BE REQUIRED,
but hangs -- this needs to be clarified as well*):
The simplified header + use/s "../ProgLang/term.sml" removed:
*** Error (line 127 of "/usr/local/isabisac/src/Tools/isac/Knowledge/Atools.thy"):
*** Value or constructor (vars) has not been declared
but now arrive at:
*** Error (line 26 of "/usr/local/isabisac/src/Tools/isac/ProgLang/term.sml"):
*** Value or constructor (indent) has not been declared
which is definitely a mess, because ProgLang/term.sml appeared
already earlier in Build_Isac.thy
     1 theory Foo_Know111 imports "../1language/Foo_Language" begin
     2 
     3 consts foo111 :: "'a"
     4        bar111 :: "'a"
     5 axioms code111 : "foo111 = bar111"
     6 
     7 ML {*
     8 (* there is an error when de-commenting *) 111
     9 *}
    10 
    11 end