equal
deleted
inserted
replaced
438 | stac2tac_ pt thy (stac as Const ("Script.SubProblem",_) $ |
438 | stac2tac_ pt thy (stac as Const ("Script.SubProblem",_) $ |
439 (Const ("Pair",_) $ |
439 (Const ("Pair",_) $ |
440 Free (dI',_) $ |
440 Free (dI',_) $ |
441 (Const ("Pair",_) $ pI' $ mI')) $ ags') = |
441 (Const ("Pair",_) $ pI' $ mI')) $ ags') = |
442 (*compare "| assod _ (Subproblem'"*) |
442 (*compare "| assod _ (Subproblem'"*) |
443 let val dI = ((implode o drop_last(*.._*) o explode) dI')^".thy"; |
443 let val dI = ((implode o drop_last(*.."'"*) o explode) dI')(*^".thy"*); |
444 val thy = maxthy (assoc_thy dI) (rootthy pt); |
444 val thy = maxthy (assoc_thy dI) (rootthy pt); |
445 val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI'; |
445 val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI'; |
446 val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI'; |
446 val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI'; |
447 val ags = isalist2list ags'; |
447 val ags = isalist2list ags'; |
448 val (pI, pors, mI) = |
448 val (pI, pors, mI) = |
706 (stac as Const ("Script.SubProblem",_) $ |
706 (stac as Const ("Script.SubProblem",_) $ |
707 (Const ("Pair",_) $ |
707 (Const ("Pair",_) $ |
708 Free (dI',_) $ |
708 Free (dI',_) $ |
709 (Const ("Pair",_) $ pI' $ mI')) $ ags') = |
709 (Const ("Pair",_) $ pI' $ mI')) $ ags') = |
710 (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*) |
710 (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*) |
711 let val dI = ((implode o drop_last o explode) dI')^".thy"; |
711 let val dI = ((implode o drop_last(*.."'"*) o explode) dI')(*^".thy"*); |
712 val thy = maxthy (assoc_thy dI) (rootthy pt); |
712 val thy = maxthy (assoc_thy dI) (rootthy pt); |
713 val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI'; |
713 val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI'; |
714 val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI'; |
714 val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI'; |
715 val ags = isalist2list ags'; |
715 val ags = isalist2list ags'; |
716 val (pI, pors, mI) = |
716 val (pI, pors, mI) = |