src/Pure/Isar/class.ML
changeset 25574 016f677ad7b8
parent 25536 01753a944433
child 25597 34860182b250
     1.1 --- a/src/Pure/Isar/class.ML	Fri Dec 07 15:08:08 2007 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Dec 07 15:08:09 2007 +0100
     1.3 @@ -827,6 +827,7 @@
     1.4  datatype instantiation = Instantiation of {
     1.5    arities: string list * sort list * sort,
     1.6    params: ((string * string) * (string * typ)) list
     1.7 +    (*(instantiation const, type constructor), (local instantiation parameter, typ)*)
     1.8  }
     1.9  
    1.10  structure Instantiation = ProofDataFun
    1.11 @@ -903,7 +904,8 @@
    1.12  
    1.13  val sanatize_name = (*FIXME*)
    1.14    let
    1.15 -    fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
    1.16 +    fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
    1.17 +      orelse s = "'" orelse s = "_";
    1.18      val is_junk = not o is_valid andf Symbol.is_regular;
    1.19      val junk = Scan.many is_junk;
    1.20      val scan_valids = Symbol.scanner "Malformed input"
    1.21 @@ -932,6 +934,7 @@
    1.22      |> ProofContext.init
    1.23      |> Instantiation.put (mk_instantiation ((tycos, sorts, sort), params))
    1.24      |> fold (Variable.declare_term o Logic.mk_type) vs
    1.25 +    |> fold (Variable.declare_names o Free o snd) params
    1.26      |> fold (fn tyco => ProofContext.add_arity (tyco, sorts, sort)) tycos
    1.27      |> Context.proof_map (
    1.28          Syntax.add_term_check 0 "instance" inst_term_check