# HG changeset patch
# User haftmann
# Date 1197036489 -3600
# Node ID 016f677ad7b8a737ad8376faed9ae85faa1e1508
# Parent  a0e695567236132364ff732033bb8351a1afbb82
declaration of instance parameter names

diff -r a0e695567236 -r 016f677ad7b8 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Dec 07 15:08:08 2007 +0100
+++ b/src/Pure/Isar/class.ML	Fri Dec 07 15:08:09 2007 +0100
@@ -827,6 +827,7 @@
 datatype instantiation = Instantiation of {
   arities: string list * sort list * sort,
   params: ((string * string) * (string * typ)) list
+    (*(instantiation const, type constructor), (local instantiation parameter, typ)*)
 }
 
 structure Instantiation = ProofDataFun
@@ -903,7 +904,8 @@
 
 val sanatize_name = (*FIXME*)
   let
-    fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'";
+    fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
+      orelse s = "'" orelse s = "_";
     val is_junk = not o is_valid andf Symbol.is_regular;
     val junk = Scan.many is_junk;
     val scan_valids = Symbol.scanner "Malformed input"
@@ -932,6 +934,7 @@
     |> ProofContext.init
     |> Instantiation.put (mk_instantiation ((tycos, sorts, sort), params))
     |> fold (Variable.declare_term o Logic.mk_type) vs
+    |> fold (Variable.declare_names o Free o snd) params
     |> fold (fn tyco => ProofContext.add_arity (tyco, sorts, sort)) tycos
     |> Context.proof_map (
         Syntax.add_term_check 0 "instance" inst_term_check