src/HOL/Tools/ATP/atp_problem.ML
changeset 46445 ef9d534e9119
parent 46443 c86276014571
child 46643 a88bccd2b567
equal deleted inserted replaced
46444:db6d2a89a21f 46445:ef9d534e9119
   318      | _ => ty)
   318      | _ => ty)
   319   | flatten_type (ty as AType _) = ty
   319   | flatten_type (ty as AType _) = ty
   320   | flatten_type _ =
   320   | flatten_type _ =
   321     raise Fail "unexpected higher-order type in first-order format"
   321     raise Fail "unexpected higher-order type in first-order format"
   322 
   322 
   323 val dfg_individual_type = "ii" (* cannot clash *)
   323 val dfg_individual_type = "iii" (* cannot clash *)
   324 
   324 
   325 fun str_for_type format ty =
   325 fun str_for_type format ty =
   326   let
   326   let
   327     val dfg = (format = DFG DFG_Sorted)
   327     val dfg = (format = DFG DFG_Sorted)
   328     fun str _ (AType (s, [])) =
   328     fun str _ (AType (s, [])) =