src/Tools/isac/Interpret/script.sml
branchdecompose-isar
changeset 42014 2863ed75b595
parent 42011 6a9ba30ab6bc
child 42015 e9af6f1bc0fc
     1.1 --- a/src/Tools/isac/Interpret/script.sml	Fri May 20 08:20:53 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri May 20 08:32:57 2011 +0200
     1.3 @@ -1632,13 +1632,13 @@
     1.4    let
     1.5      val p' = par_pblobj pt p
     1.6  	  val thy = assoc_thy thy'
     1.7 -	  val PblObj {meth=itms, ctxt, ...} = get_obj I pt p'
     1.8 +	  val PblObj {meth=itms, ...} = get_obj I pt p'
     1.9  	  val metID = get_obj g_metID pt p'
    1.10  	  val {srls,scr,...} = get_met metID
    1.11    in
    1.12      if last_elem p = 0 (*nothing written to pt yet*)
    1.13      then
    1.14 -       let val (is, _, scr) = init_scrstate thy itms metID
    1.15 +       let val (is, ctxt, scr) = init_scrstate thy itms metID
    1.16  	     in (srls, (is, ctxt), scr) end
    1.17         else (srls, get_loc pt (p,p_), scr)
    1.18      end;