1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Apr 29 12:43:50 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Apr 29 14:13:11 2021 +0200
     1.3 @@ -25,6 +25,7 @@
     1.4    'bdv' is a constant handled on the meta-level 
     1.5     specifically as a 'bound variable'            *)
     1.6  
     1.7 +(*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
     1.8    integral_const:    "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" and
     1.9    integral_var:      "Integral bdv D bdv = bdv \<up> 2 / 2" and
    1.10  
    1.11 @@ -37,6 +38,7 @@
    1.12  		     a = a + new_c a"
    1.13  *)
    1.14    integral_pow:      "Integral bdv \<up> n D bdv = bdv \<up> (n+1) / (n + 1)"
    1.15 +(*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
    1.16  
    1.17  ML \<open>
    1.18  val thy = @{theory};
    1.19 @@ -63,7 +65,7 @@
    1.20      in 
    1.21  	case cs of
    1.22  	    [] => c
    1.23 -	  | [c] => Free ("c_2", HOLogic.realT)
    1.24 +	  | [_] => Free ("c_2", HOLogic.realT)
    1.25  	  | cs => 
    1.26  	    let val max_coeff = maxl (map get_coeff cs)
    1.27  	    in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end