1.1 --- a/src/Tools/isac/Interpret/ctree.sml	Sun May 15 10:25:42 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Sun May 15 11:32:41 2011 +0200
     1.3 @@ -274,7 +274,10 @@
     1.4         | ScrState of scrstate    (*for script interpreter*)
     1.5         | RrlsState of rrlsstate; (*for reverse rewriting*)
     1.6  val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false)):istate;
     1.7 -val e_ctxt = ProofContext.init_global @{theory};
     1.8 +val e_ctxt = ProofContext.init_global @{theory "Pure"};
     1.9 +
    1.10 +(* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)
    1.11 +fun is_e_ctxt ctxt = Theory.eq_thy (ProofContext.theory_of ctxt, @{theory "Pure"});
    1.12  
    1.13  type iist = istate option * istate option;
    1.14  (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)