1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Sun Sep 22 16:52:14 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Sep 26 17:47:10 2019 +0200
     1.3 @@ -181,9 +181,9 @@
     1.4      equs = SubProblem (''Biegelinie'', [''setzeRandbedingungen'', ''Biegelinien''],
     1.5               [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST s];
     1.6      cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''], [''no_met''])
     1.7 -             [BOOL_LIST equs, REAL_LIST vs];     \<comment> \<open>PROG consts\<close>
     1.8 +             [BOOL_LIST equs, REAL_LIST vs];
     1.9      B = Take (lastI funs);
    1.10 -    B = ((Substitute cons) @@ (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B                         
    1.11 +    B = ((Substitute cons) @@ (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B
    1.12    in B)"
    1.13  setup \<open>KEStore_Elems.add_mets
    1.14      [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID