diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Knowledge/DiffApp-scrpbl.sml
--- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Thu Dec 22 11:12:18 2016 +0100
+++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml	Thu Dec 22 11:36:20 2016 +0100
@@ -420,7 +420,7 @@
 val p = e_pos'; val c = []; 
 
 val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI')));
-val (pst as (sc,pt,cl):pstate) = (EmptyScr, e_ptree, []);
+val (pst as (sc,pt,cl):pstate) = (EmptyScr, e_ctree, []);
 val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst;
 (*val nxt = ("Add_Given",Add_Given "fixedValues [R = R]")*)