src/Tools/isac/Interpret/script.sml
branchdecompose-isar
changeset 42082 2556b7865f9b
parent 42023 927cb6806af1
child 42092 1a6d6089e594
     1.1 --- a/src/Tools/isac/Interpret/script.sml	Wed Jul 13 10:41:17 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Thu Jul 14 09:33:57 2011 +0200
     1.3 @@ -1590,7 +1590,7 @@
     1.4     (*3*) from rls/PrfObj: in case of detail a ruleset *)
     1.5  fun from_pblobj_or_detail' thy' (p,p_) pt =
     1.6    let val ctxt = get_ctxt pt (p,p_)
     1.7 -    in
     1.8 +  in
     1.9      if member op = [Pbl,Met] p_
    1.10      then case get_obj g_env pt p of
    1.11    	       NONE => error "from_pblobj_or_detail': no istate"
    1.12 @@ -1618,7 +1618,7 @@
    1.13  	  	          Rls {scr=scr,...} => scr
    1.14  	            | Seq {scr=scr,...} => scr
    1.15  	            | Rrls {scr=rfuns,...} => rfuns)
    1.16 -    end
    1.17 +      end
    1.18    end;
    1.19  
    1.20  (*.get script and istate from PblObj, see                        (*1*) above.*)